85 fun ouput_response_fake_both _ (lhs, pat) = |
85 fun ouput_response_fake_both _ (lhs, pat) = |
86 output ((split_lines lhs) @ (prefix_lines "> " pat)) |
86 output ((split_lines lhs) @ (prefix_lines "> " pat)) |
87 |
87 |
88 val single_arg = Scan.lift (Args.name) |
88 val single_arg = Scan.lift (Args.name) |
89 val two_args = Scan.lift (Args.name -- Args.name) |
89 val two_args = Scan.lift (Args.name -- Args.name) |
|
90 val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with" |-- Args.name)) |
90 |
91 |
91 val _ = ThyOutput.antiquotation "ML" parser_ml output_ml |
92 val _ = ThyOutput.antiquotation "ML" parser_ml output_ml |
92 val _ = ThyOutput.antiquotation "ML_ind" parser_ml_ind output_ml_ind |
93 val _ = ThyOutput.antiquotation "ML_ind" parser_ml_ind output_ml_ind |
93 val _ = ThyOutput.antiquotation "ML_type" single_arg output_type |
94 val _ = ThyOutput.antiquotation "ML_type" single_arg output_type |
94 val _ = ThyOutput.antiquotation "ML_type_ind" single_arg output_type_ind |
95 val _ = ThyOutput.antiquotation "ML_type_ind" single_arg output_type_ind |
96 val _ = ThyOutput.antiquotation "ML_struct_ind" single_arg output_struct_ind |
97 val _ = ThyOutput.antiquotation "ML_struct_ind" single_arg output_struct_ind |
97 val _ = ThyOutput.antiquotation "ML_response" two_args output_response |
98 val _ = ThyOutput.antiquotation "ML_response" two_args output_response |
98 val _ = ThyOutput.antiquotation "ML_response_fake" two_args output_response_fake |
99 val _ = ThyOutput.antiquotation "ML_response_fake" two_args output_response_fake |
99 val _ = ThyOutput.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both |
100 val _ = ThyOutput.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both |
100 |
101 |
|
102 (* FIXME: experimental *) |
|
103 fun ml_eq (lhs, pat, eq) = |
|
104 implode ["val true = ((", eq, ") (", lhs, ",", pat, "))"] |
|
105 |
|
106 fun output_response_eq {context = ctxt, ...} ((lhs, pat), eq) = |
|
107 (case eq of |
|
108 NONE => eval_fn ctxt (ml_pat (lhs, pat)) |
|
109 | SOME e => eval_fn ctxt (ml_eq (lhs, pat, e)); |
|
110 output ((prefix_lines "" lhs) @ (prefix_lines "> " pat))) |
|
111 |
|
112 val _ = ThyOutput.antiquotation "ML_response_eq" test output_response_eq |
|
113 |
|
114 (* checks whether a file exists in the Isabelle distribution *) |
101 fun href_link txt = |
115 fun href_link txt = |
102 let |
116 let |
103 val raw = Symbol.encode_raw |
117 val raw = Symbol.encode_raw |
104 val path = "http://isabelle.in.tum.de/repos/isabelle/raw-file/tip/src/" |
118 val path = "http://isabelle.in.tum.de/repos/isabelle/raw-file/tip/src/" |
105 in |
119 in |
106 implode [raw "\\href{", raw path, raw txt, raw "}{", txt, raw "}"] |
120 implode [raw "\\href{", raw path, raw txt, raw "}{", txt, raw "}"] |
107 end |
121 end |
108 |
122 |
109 (* checks whether a file exists in the Isabelle distribution *) |
|
110 fun check_file_exists _ txt = |
123 fun check_file_exists _ txt = |
111 (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) |
124 (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) |
112 then output [href_link txt] |
125 then output [href_link txt] |
113 else error (implode ["Source file ", quote txt, " does not exist."])) |
126 else error (implode ["Source file ", quote txt, " does not exist."])) |
114 |
|
115 |
127 |
116 val _ = ThyOutput.antiquotation "ML_file" single_arg check_file_exists |
128 val _ = ThyOutput.antiquotation "ML_file" single_arg check_file_exists |
117 |
129 |
118 |
130 |
119 (* replaces the official subgoal antiquotation with one *) |
131 (* replaces the official subgoal antiquotation with one *) |