equal
deleted
inserted
replaced
78 val _ = ThyOutput.antiquotation "ML_struct" single_arg (output_exp ml_struct) |
78 val _ = ThyOutput.antiquotation "ML_struct" single_arg (output_exp ml_struct) |
79 val _ = ThyOutput.antiquotation "ML_response" two_args output_response |
79 val _ = ThyOutput.antiquotation "ML_response" two_args output_response |
80 val _ = ThyOutput.antiquotation "ML_response_fake" two_args output_response_fake |
80 val _ = ThyOutput.antiquotation "ML_response_fake" two_args output_response_fake |
81 val _ = ThyOutput.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both |
81 val _ = ThyOutput.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both |
82 |
82 |
|
83 fun href_link txt = |
|
84 let |
|
85 val raw = Symbol.encode_raw |
|
86 val path = "http://isabelle.in.tum.de/repos/isabelle/raw-file/tip/src/" |
|
87 in |
|
88 (raw "\\href{") ^ (raw path) ^ (raw txt) ^ (raw "}{") ^ txt ^ (raw "}") |
|
89 end |
|
90 |
83 (* checks whether a file exists in the Isabelle distribution *) |
91 (* checks whether a file exists in the Isabelle distribution *) |
84 fun check_file_exists _ txt = |
92 fun check_file_exists _ txt = |
85 (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) |
93 (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) |
86 then output_fn (string_explode "" txt) |
94 then output_fn [href_link txt] |
87 else error ("Source file " ^ (quote txt) ^ " does not exist.")) |
95 else error ("Source file " ^ (quote txt) ^ " does not exist.")) |
88 |
96 |
89 val _ = ThyOutput.antiquotation "ML_file" single_arg check_file_exists |
97 val _ = ThyOutput.antiquotation "ML_file" single_arg check_file_exists |
90 |
98 |
91 |
99 |