29 implode ["functor DUMMY_FUNCTOR() = struct structure DUMMY = ", txt, " end"] |
29 implode ["functor DUMMY_FUNCTOR() = struct structure DUMMY = ", txt, " end"] |
30 |
30 |
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 fun ml_out txt = |
|
35 implode ["val _ = Pretty.writeln ((Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation ((", txt, "), ML_Options.get_print_depth ()))))) handle _ => writeln \"exception\""] |
|
36 |
|
37 (* eval function *) |
34 (* eval function *) |
38 fun eval_fn ctxt exp = |
35 fun eval_fn ctxt exp = |
39 ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags |
36 ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags |
40 {delimited = false, text = exp, pos = Position.none} |
37 (Input.source false exp Position.no_range) |
41 |
38 |
42 (* checks and prints a possibly open expressions, no index *) |
39 (* checks and prints a possibly open expressions, no index *) |
43 fun output_ml {context = ctxt, ...} (txt, (vs, stru)) = |
40 fun output_ml ctxt (txt, (vs, stru)) = |
44 (eval_fn ctxt (ml_val vs stru txt); |
41 (eval_fn ctxt (ml_val vs stru txt); |
45 output ctxt (split_lines txt)) |
42 output ctxt (split_lines txt)) |
46 |
43 |
47 val parser_ml = Scan.lift (Args.name -- |
44 val parser_ml = Scan.lift (Args.name -- |
48 (Scan.optional (Args.$$$ "for" |-- Parse.!!! (Scan.repeat1 Args.name)) [] -- |
45 (Scan.optional (Args.$$$ "for" |-- Parse.!!! (Scan.repeat1 Args.name)) [] -- |
49 Scan.option (Args.$$$ "in" |-- Parse.!!! Args.name))) |
46 Scan.option (Args.$$$ "in" |-- Parse.!!! Args.name))) |
50 |
47 |
51 (* checks and prints a single ML-item and produces an index entry *) |
48 (* checks and prints a single ML-item and produces an index entry *) |
52 fun output_ml_ind {context = ctxt, ...} (txt, stru) = |
49 fun output_ml_ind ctxt (txt, stru) = |
53 (eval_fn ctxt (ml_val [] stru txt); |
50 (eval_fn ctxt (ml_val [] stru txt); |
54 case (stru, Long_Name.base_name txt, Long_Name.qualifier txt) of |
51 case (stru, Long_Name.base_name txt, Long_Name.qualifier txt) of |
55 (NONE, bn, "") => output_indexed ctxt {main = Code txt, minor = NoString} (split_lines txt) |
52 (NONE, _, "") => output_indexed ctxt {main = Code txt, minor = NoString} (split_lines txt) |
56 | (NONE, bn, qn) => output_indexed ctxt {main = Code bn, minor = Struct qn} (split_lines txt) |
53 | (NONE, bn, qn) => output_indexed ctxt {main = Code bn, minor = Struct qn} (split_lines txt) |
57 | (SOME st, _, _) => output_indexed ctxt {main = Code txt, minor = Struct st} (split_lines txt)) |
54 | (SOME st, _, _) => output_indexed ctxt {main = Code txt, minor = Struct st} (split_lines txt)) |
58 |
55 |
59 val parser_ml_ind = Scan.lift (Args.name -- |
56 val parser_ml_ind = Scan.lift (Args.name -- |
60 Scan.option (Args.$$$ "in" |-- Parse.!!! Args.name)) |
57 Scan.option (Args.$$$ "in" |-- Parse.!!! Args.name)) |
62 (* checks and prints structures *) |
59 (* checks and prints structures *) |
63 fun gen_output_struct outfn ctxt txt = |
60 fun gen_output_struct outfn ctxt txt = |
64 (eval_fn ctxt (ml_struct txt); |
61 (eval_fn ctxt (ml_struct txt); |
65 outfn {main = Code txt, minor = Plain "structure"} (split_lines txt)) |
62 outfn {main = Code txt, minor = Plain "structure"} (split_lines txt)) |
66 |
63 |
67 fun output_struct {context = ctxt, ...} = gen_output_struct (K (output ctxt)) ctxt |
64 fun output_struct ctxt = gen_output_struct (K (output ctxt)) ctxt |
68 fun output_struct_ind {context = ctxt, ...} = gen_output_struct (output_indexed ctxt) ctxt |
65 fun output_struct_ind ctxt = gen_output_struct (output_indexed ctxt) ctxt |
69 |
66 |
70 (* prints functors; no checks *) |
67 (* prints functors; no checks *) |
71 fun gen_output_funct outfn txt = |
68 fun gen_output_funct outfn txt = |
72 (outfn {main = Code txt, minor = Plain "functor"} (split_lines txt)) |
69 (outfn {main = Code txt, minor = Plain "functor"} (split_lines txt)) |
73 |
70 |
74 fun output_funct {context = ctxt, ...} = gen_output_funct (K (output ctxt)) |
71 fun output_funct ctxt = gen_output_funct (K (output ctxt)) |
75 fun output_funct_ind {context = ctxt, ...} = gen_output_funct (output_indexed ctxt) |
72 fun output_funct_ind ctxt = gen_output_funct (output_indexed ctxt) |
76 |
73 |
77 (* checks and prints types *) |
74 (* checks and prints types *) |
78 fun gen_output_type outfn ctxt txt = |
75 fun gen_output_type outfn ctxt txt = |
79 (eval_fn ctxt (ml_type txt); |
76 (eval_fn ctxt (ml_type txt); |
80 outfn {main = Code txt, minor = Plain "type"} (split_lines txt)) |
77 outfn {main = Code txt, minor = Plain "type"} (split_lines txt)) |
81 |
78 |
82 fun output_type {context = ctxt, ...} = gen_output_type (K (output ctxt)) ctxt |
79 fun output_type ctxt = gen_output_type (K (output ctxt)) ctxt |
83 fun output_type_ind {context = ctxt, ...} = gen_output_type (output_indexed ctxt) ctxt |
80 fun output_type_ind ctxt = gen_output_type (output_indexed ctxt) ctxt |
84 |
81 |
85 (* checks and expression agains a result pattern *) |
82 (* checks and expression agains a result pattern *) |
86 fun output_response {context = ctxt, ...} (lhs, pat) = |
83 fun output_response ctxt (lhs, pat) = |
87 (eval_fn ctxt (ml_pat (lhs, pat)); |
84 (eval_fn ctxt (ml_pat (lhs, pat)); |
88 eval_fn ctxt (ml_out lhs); |
85 (*eval_fn ctxt (ml_out lhs);*) (*FIXME remove*) |
89 output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat))) |
86 output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat))) |
90 |
87 |
91 (* checks the expressions, but does not check it against a result pattern *) |
88 (* checks the expressions, but does not check it against a result pattern *) |
92 fun output_response_fake {context = ctxt, ...} (lhs, pat) = |
89 fun output_response_fake ctxt (lhs, pat) = |
93 (eval_fn ctxt (ml_val [] NONE lhs); |
90 (eval_fn ctxt (ml_val [] NONE lhs); |
94 eval_fn ctxt (ml_out lhs); |
91 (*eval_fn ctxt (ml_out lhs);*) (* FIXME remove *) |
95 output ctxt ((split_lines lhs) @ (prefix_lines "> " pat))) |
92 output ctxt ((split_lines lhs) @ (prefix_lines "> " pat))) |
96 |
93 |
97 (* checks the expressions, but does not check it against a result pattern *) |
94 (* checks the expressions, but does not check it against a result pattern *) |
98 fun ouput_response_fake_both {context = ctxt, ...} (lhs, pat) = |
95 fun ouput_response_fake_both ctxt (lhs, pat) = |
99 (output ctxt ((split_lines lhs) @ (prefix_lines "> " pat))) |
96 (output ctxt ((split_lines lhs) @ (prefix_lines "> " pat))) |
100 |
97 |
101 val single_arg = Scan.lift (Args.name) |
98 val single_arg = Scan.lift (Args.name) |
102 val two_args = Scan.lift (Args.name -- Args.name) |
99 val two_args = Scan.lift (Args.name -- Args.name) |
103 val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with" |-- Args.name)) |
100 val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with" |-- Args.name)) |
104 |
101 |
|
102 |
|
103 |
|
104 |
105 val ml_setup = |
105 val ml_setup = |
106 Thy_Output.antiquotation @{binding "ML"} parser_ml output_ml |
106 Thy_Output.antiquotation_raw @{binding "ML"} parser_ml output_ml |
107 #> Thy_Output.antiquotation @{binding "ML_ind"} parser_ml_ind output_ml_ind |
107 #> Thy_Output.antiquotation_raw @{binding "ML_ind"} parser_ml_ind output_ml_ind |
108 #> Thy_Output.antiquotation @{binding "ML_type"} single_arg output_type |
108 #> Thy_Output.antiquotation_raw @{binding "ML_type"} single_arg output_type |
109 #> Thy_Output.antiquotation @{binding "ML_type_ind"} single_arg output_type_ind |
109 #> Thy_Output.antiquotation_raw @{binding "ML_type_ind"} single_arg output_type_ind |
110 #> Thy_Output.antiquotation @{binding "ML_struct"} single_arg output_struct |
110 #> Thy_Output.antiquotation_raw @{binding "ML_struct"} single_arg output_struct |
111 #> Thy_Output.antiquotation @{binding "ML_struct_ind"} single_arg output_struct_ind |
111 #> Thy_Output.antiquotation_raw @{binding "ML_struct_ind"} single_arg output_struct_ind |
112 #> Thy_Output.antiquotation @{binding "ML_funct"} single_arg output_funct |
112 #> Thy_Output.antiquotation_raw @{binding "ML_funct"} single_arg output_funct |
113 #> Thy_Output.antiquotation @{binding "ML_funct_ind"} single_arg output_funct_ind |
113 #> Thy_Output.antiquotation_raw @{binding "ML_funct_ind"} single_arg output_funct_ind |
114 #> Thy_Output.antiquotation @{binding "ML_response"} two_args output_response |
114 #> Thy_Output.antiquotation_raw @{binding "ML_response"} two_args output_response |
115 #> Thy_Output.antiquotation @{binding "ML_response_fake"} two_args output_response_fake |
115 #> Thy_Output.antiquotation_raw @{binding "ML_response_fake"} two_args output_response_fake |
116 #> Thy_Output.antiquotation @{binding "ML_response_fake_both"} two_args ouput_response_fake_both |
116 #> Thy_Output.antiquotation_raw @{binding "ML_response_fake_both"} two_args ouput_response_fake_both |
117 |
117 |
118 (* FIXME: experimental *) |
118 (* FIXME: experimental *) |
119 fun ml_eq (lhs, pat, eq) = |
119 fun ml_eq (lhs, pat, eq) = |
120 implode ["val true = ((", eq, ") (", lhs, ",", pat, "))"] |
120 implode ["val true = ((", eq, ") (", lhs, ",", pat, "))"] |
121 |
121 |
122 fun output_response_eq {context = ctxt, ...} ((lhs, pat), eq) = |
122 fun output_response_eq ctxt ((lhs, pat), eq) = |
123 (case eq of |
123 (case eq of |
124 NONE => eval_fn ctxt (ml_pat (lhs, pat)) |
124 NONE => eval_fn ctxt (ml_pat (lhs, pat)) |
125 | SOME e => eval_fn ctxt (ml_eq (lhs, pat, e)); |
125 | SOME e => eval_fn ctxt (ml_eq (lhs, pat, e)); |
126 output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat))) |
126 output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat))) |
127 |
127 |
128 val ml_response_setup = |
128 val ml_response_setup = |
129 Thy_Output.antiquotation @{binding "ML_response_eq"} test output_response_eq |
129 Thy_Output.antiquotation_raw @{binding "ML_response_eq"} test output_response_eq |
130 |
130 |
131 (* checks whether a file exists in the Isabelle distribution *) |
131 (* checks whether a file exists in the Isabelle distribution *) |
132 fun href_link txt = |
132 fun href_link txt = |
133 let |
133 let |
134 val raw = Symbol.encode_raw |
134 val raw = I (* FIXME: Symbol.encode_raw *) |
135 val path = "http://isabelle.in.tum.de/repos/isabelle/raw-file/tip/src/" |
135 val path = "http://isabelle.in.tum.de/repos/isabelle/raw-file/tip/src/" |
136 in |
136 in |
137 implode [raw "\\href{", raw path, raw txt, raw "}{", txt, raw "}"] |
137 implode [raw "\\href{", raw path, raw txt, raw "}{", get_word txt, raw "}"] |
138 end |
138 end |
139 |
139 |
140 fun check_file_exists {context = ctxt, ...} txt = |
140 fun check_file_exists _ txt = |
141 (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) |
141 (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) |
142 then output ctxt [href_link txt] |
142 then Latex.string (href_link txt) |
143 else error (implode ["Source file ", quote txt, " does not exist."])) |
143 else error (implode ["Source file ", quote txt, " does not exist."])) |
144 |
144 |
145 val ml_file_setup = Thy_Output.antiquotation @{binding "ML_file"} single_arg check_file_exists |
145 val ml_file_setup = Thy_Output.antiquotation_raw @{binding "ML_file"} single_arg check_file_exists |
146 |
146 |
147 |
147 |
148 (* replaces the official subgoal antiquotation with one *) |
148 (* replaces the official subgoal antiquotation with one *) |
149 (* that is closer to the actual output *) |
149 (* that is closer to the actual output *) |
|
150 |
150 fun proof_state state = |
151 fun proof_state state = |
151 (case try (Proof.goal o Toplevel.proof_of) state of |
152 (case try (Proof.goal o Toplevel.proof_of) state of |
152 SOME {goal, ...} => goal |
153 SOME {goal, ...} => goal |
153 | _ => error "No proof state"); |
154 | _ => error "No proof state"); |
154 |
155 |
155 |
156 |
156 fun output_goals {state = node, context = ctxt, ...} _ = |
157 fun output_goals ctxt _ = |
157 let |
158 let |
158 fun subgoals 0 = "" |
159 fun subgoals 0 = "" |
159 | subgoals 1 = "goal (1 subgoal):" |
160 | subgoals 1 = "goal (1 subgoal):" |
160 | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):" |
161 | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):" |
161 |
162 |
162 val state = proof_state node |
163 val state = proof_state (Toplevel.presentation_state ctxt) |
163 val goals = Goal_Display.pretty_goal ctxt state |
164 val goals = Goal_Display.pretty_goal ctxt state |
164 |
165 |
165 val {prop, ...} = rep_thm state; |
166 val prop = Thm.prop_of state; |
166 val (As, _) = Logic.strip_horn prop; |
167 val (As, _) = Logic.strip_horn prop; |
167 val output = (case (length As) of |
168 val out = (case (length As) of |
168 0 => [goals] |
169 0 => goals |
169 | n => [Pretty.str (subgoals n), goals]) |
170 | n => Pretty.big_list (subgoals n) [goals]) (* FIXME: improve printing? *) |
170 in |
171 in |
171 Thy_Output.output ctxt output |
172 output ctxt [Pretty.string_of out] |
172 end |
173 end |
173 |
174 |
174 |
175 |
175 fun output_raw_goal_state {state, context = ctxt, ...} _ = |
176 fun output_raw_goal_state ctxt _ = |
176 let |
177 let |
177 val goals = proof_state state |
178 val goals = proof_state (Toplevel.presentation_state ctxt) |
178 val output = [Pretty.str (Syntax.string_of_term ctxt (prop_of goals))] |
179 val out = Syntax.string_of_term ctxt (Thm.prop_of goals) |
179 in |
180 in |
180 Thy_Output.output ctxt output |
181 output ctxt [out] |
181 end |
182 end |
182 |
183 |
183 val subgoals_setup = |
184 val subgoals_setup = |
184 Thy_Output.antiquotation @{binding "subgoals"} (Scan.succeed ()) output_goals |
185 Thy_Output.antiquotation_raw @{binding "subgoals"} (Scan.succeed ()) output_goals |
185 val raw_goal_state_setup = |
186 val raw_goal_state_setup = |
186 Thy_Output.antiquotation @{binding "raw_goal_state"} (Scan.succeed ()) output_raw_goal_state |
187 Thy_Output.antiquotation_raw @{binding "raw_goal_state"} (Scan.succeed ()) output_raw_goal_state |
187 |
188 |
188 val setup = |
189 val setup = |
189 ml_setup #> |
190 ml_setup #> |
190 ml_response_setup #> |
191 ml_response_setup #> |
191 ml_file_setup #> |
192 ml_file_setup #> |