31 fun ml_type txt = |
31 fun ml_type txt = |
32 implode ["val _ = NONE : (", txt, ") option"]; |
32 implode ["val _ = NONE : (", txt, ") option"]; |
33 |
33 |
34 (* eval function *) |
34 (* eval function *) |
35 fun eval_fn ctxt exp = |
35 fun eval_fn ctxt exp = |
36 ML_Context.eval_in (SOME ctxt) false Position.none exp |
36 ML_Context.eval_text_in (SOME ctxt) false Position.none exp |
37 |
37 |
38 (* checks and prints a possibly open expressions, no index *) |
38 (* checks and prints a possibly open expressions, no index *) |
39 fun output_ml {context = ctxt, ...} (txt, (vs, stru)) = |
39 fun output_ml {context = ctxt, ...} (txt, (vs, stru)) = |
40 (eval_fn ctxt (ml_val vs stru txt); |
40 (eval_fn ctxt (ml_val vs stru txt); |
41 output (split_lines txt)) |
41 output (split_lines txt)) |
96 |
96 |
97 val single_arg = Scan.lift (Args.name) |
97 val single_arg = Scan.lift (Args.name) |
98 val two_args = Scan.lift (Args.name -- Args.name) |
98 val two_args = Scan.lift (Args.name -- Args.name) |
99 val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with" |-- Args.name)) |
99 val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with" |-- Args.name)) |
100 |
100 |
101 val _ = ThyOutput.antiquotation "ML" parser_ml output_ml |
101 val _ = Thy_Output.antiquotation "ML" parser_ml output_ml |
102 val _ = ThyOutput.antiquotation "ML_ind" parser_ml_ind output_ml_ind |
102 val _ = Thy_Output.antiquotation "ML_ind" parser_ml_ind output_ml_ind |
103 val _ = ThyOutput.antiquotation "ML_type" single_arg output_type |
103 val _ = Thy_Output.antiquotation "ML_type" single_arg output_type |
104 val _ = ThyOutput.antiquotation "ML_type_ind" single_arg output_type_ind |
104 val _ = Thy_Output.antiquotation "ML_type_ind" single_arg output_type_ind |
105 val _ = ThyOutput.antiquotation "ML_struct" single_arg output_struct |
105 val _ = Thy_Output.antiquotation "ML_struct" single_arg output_struct |
106 val _ = ThyOutput.antiquotation "ML_struct_ind" single_arg output_struct_ind |
106 val _ = Thy_Output.antiquotation "ML_struct_ind" single_arg output_struct_ind |
107 val _ = ThyOutput.antiquotation "ML_funct" single_arg output_funct |
107 val _ = Thy_Output.antiquotation "ML_funct" single_arg output_funct |
108 val _ = ThyOutput.antiquotation "ML_funct_ind" single_arg output_funct_ind |
108 val _ = Thy_Output.antiquotation "ML_funct_ind" single_arg output_funct_ind |
109 val _ = ThyOutput.antiquotation "ML_response" two_args output_response |
109 val _ = Thy_Output.antiquotation "ML_response" two_args output_response |
110 val _ = ThyOutput.antiquotation "ML_response_fake" two_args output_response_fake |
110 val _ = Thy_Output.antiquotation "ML_response_fake" two_args output_response_fake |
111 val _ = ThyOutput.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both |
111 val _ = Thy_Output.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both |
112 |
112 |
113 (* FIXME: experimental *) |
113 (* FIXME: experimental *) |
114 fun ml_eq (lhs, pat, eq) = |
114 fun ml_eq (lhs, pat, eq) = |
115 implode ["val true = ((", eq, ") (", lhs, ",", pat, "))"] |
115 implode ["val true = ((", eq, ") (", lhs, ",", pat, "))"] |
116 |
116 |
118 (case eq of |
118 (case eq of |
119 NONE => eval_fn ctxt (ml_pat (lhs, pat)) |
119 NONE => eval_fn ctxt (ml_pat (lhs, pat)) |
120 | SOME e => eval_fn ctxt (ml_eq (lhs, pat, e)); |
120 | SOME e => eval_fn ctxt (ml_eq (lhs, pat, e)); |
121 output ((prefix_lines "" lhs) @ (prefix_lines "> " pat))) |
121 output ((prefix_lines "" lhs) @ (prefix_lines "> " pat))) |
122 |
122 |
123 val _ = ThyOutput.antiquotation "ML_response_eq" test output_response_eq |
123 val _ = Thy_Output.antiquotation "ML_response_eq" test output_response_eq |
124 |
124 |
125 (* checks whether a file exists in the Isabelle distribution *) |
125 (* checks whether a file exists in the Isabelle distribution *) |
126 fun href_link txt = |
126 fun href_link txt = |
127 let |
127 let |
128 val raw = Symbol.encode_raw |
128 val raw = Symbol.encode_raw |
134 fun check_file_exists _ txt = |
134 fun check_file_exists _ txt = |
135 (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) |
135 (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) |
136 then output [href_link txt] |
136 then output [href_link txt] |
137 else error (implode ["Source file ", quote txt, " does not exist."])) |
137 else error (implode ["Source file ", quote txt, " does not exist."])) |
138 |
138 |
139 val _ = ThyOutput.antiquotation "ML_file" single_arg check_file_exists |
139 val _ = Thy_Output.antiquotation "ML_file" single_arg check_file_exists |
140 |
140 |
141 |
141 |
142 (* replaces the official subgoal antiquotation with one *) |
142 (* replaces the official subgoal antiquotation with one *) |
143 (* that is closer to the actual output *) |
143 (* that is closer to the actual output *) |
144 fun proof_state state = |
144 fun proof_state state = |
159 val (As, _) = Logic.strip_horn prop; |
159 val (As, _) = Logic.strip_horn prop; |
160 val output = (case (length As) of |
160 val output = (case (length As) of |
161 0 => [goals] |
161 0 => [goals] |
162 | n => [Pretty.str (subgoals n), goals]) |
162 | n => [Pretty.str (subgoals n), goals]) |
163 in |
163 in |
164 ThyOutput.output output |
164 Thy_Output.output output |
165 end |
165 end |
166 |
166 |
167 fun output_raw_goal_state {state = node, context = ctxt, ...} _ = |
167 fun output_raw_goal_state {state = node, context = ctxt, ...} _ = |
168 let |
168 let |
169 val state = proof_state node; |
169 val state = proof_state node; |
171 |
171 |
172 val output = [Pretty.str (Syntax.string_of_term ctxt (prop_of goals))] |
172 val output = [Pretty.str (Syntax.string_of_term ctxt (prop_of goals))] |
173 val _ = tracing (Syntax.string_of_term ctxt (prop_of goals)) |
173 val _ = tracing (Syntax.string_of_term ctxt (prop_of goals)) |
174 val _ = tracing (Pretty.string_of (Pretty.str (Syntax.string_of_term ctxt (prop_of goals)))) |
174 val _ = tracing (Pretty.string_of (Pretty.str (Syntax.string_of_term ctxt (prop_of goals)))) |
175 in |
175 in |
176 ThyOutput.output output |
176 Thy_Output.output output |
177 end |
177 end |
178 |
178 |
179 val _ = ThyOutput.antiquotation "subgoals" (Scan.succeed ()) output_goals |
179 val _ = Thy_Output.antiquotation "subgoals" (Scan.succeed ()) output_goals |
180 val _ = ThyOutput.antiquotation "raw_goal_state" (Scan.succeed ()) output_raw_goal_state |
180 val _ = Thy_Output.antiquotation "raw_goal_state" (Scan.succeed ()) output_raw_goal_state |
181 |
181 |
182 end; |
182 end; |