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 _ = Thy_Output.antiquotation @{binding "ML"} parser_ml output_ml |
101 val ml_setup = |
102 val _ = Thy_Output.antiquotation @{binding "ML_ind"} parser_ml_ind output_ml_ind |
102 Thy_Output.antiquotation @{binding "ML"} parser_ml output_ml |
103 val _ = Thy_Output.antiquotation @{binding "ML_type"} single_arg output_type |
103 #> Thy_Output.antiquotation @{binding "ML_ind"} parser_ml_ind output_ml_ind |
104 val _ = Thy_Output.antiquotation @{binding "ML_type_ind"} single_arg output_type_ind |
104 #> Thy_Output.antiquotation @{binding "ML_type"} single_arg output_type |
105 val _ = Thy_Output.antiquotation @{binding "ML_struct"} single_arg output_struct |
105 #> Thy_Output.antiquotation @{binding "ML_type_ind"} single_arg output_type_ind |
106 val _ = Thy_Output.antiquotation @{binding "ML_struct_ind"} single_arg output_struct_ind |
106 #> Thy_Output.antiquotation @{binding "ML_struct"} single_arg output_struct |
107 val _ = Thy_Output.antiquotation @{binding "ML_funct"} single_arg output_funct |
107 #> Thy_Output.antiquotation @{binding "ML_struct_ind"} single_arg output_struct_ind |
108 val _ = Thy_Output.antiquotation @{binding "ML_funct_ind"} single_arg output_funct_ind |
108 #> Thy_Output.antiquotation @{binding "ML_funct"} single_arg output_funct |
109 val _ = Thy_Output.antiquotation @{binding "ML_response"} two_args output_response |
109 #> Thy_Output.antiquotation @{binding "ML_funct_ind"} single_arg output_funct_ind |
110 val _ = Thy_Output.antiquotation @{binding "ML_response_fake"} two_args output_response_fake |
110 #> Thy_Output.antiquotation @{binding "ML_response"} two_args output_response |
111 val _ = Thy_Output.antiquotation @{binding "ML_response_fake_both"} two_args ouput_response_fake_both |
111 #> Thy_Output.antiquotation @{binding "ML_response_fake"} two_args output_response_fake |
|
112 #> Thy_Output.antiquotation @{binding "ML_response_fake_both"} two_args ouput_response_fake_both |
112 |
113 |
113 (* FIXME: experimental *) |
114 (* FIXME: experimental *) |
114 fun ml_eq (lhs, pat, eq) = |
115 fun ml_eq (lhs, pat, eq) = |
115 implode ["val true = ((", eq, ") (", lhs, ",", pat, "))"] |
116 implode ["val true = ((", eq, ") (", lhs, ",", pat, "))"] |
116 |
117 |
118 (case eq of |
119 (case eq of |
119 NONE => eval_fn ctxt (ml_pat (lhs, pat)) |
120 NONE => eval_fn ctxt (ml_pat (lhs, pat)) |
120 | SOME e => eval_fn ctxt (ml_eq (lhs, pat, e)); |
121 | SOME e => eval_fn ctxt (ml_eq (lhs, pat, e)); |
121 output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat))) |
122 output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat))) |
122 |
123 |
123 val _ = Thy_Output.antiquotation @{binding "ML_response_eq"} test output_response_eq |
124 val ml_response_setup = |
|
125 Thy_Output.antiquotation @{binding "ML_response_eq"} test output_response_eq |
124 |
126 |
125 (* checks whether a file exists in the Isabelle distribution *) |
127 (* checks whether a file exists in the Isabelle distribution *) |
126 fun href_link txt = |
128 fun href_link txt = |
127 let |
129 let |
128 val raw = Symbol.encode_raw |
130 val raw = Symbol.encode_raw |
134 fun check_file_exists {context = ctxt, ...} txt = |
136 fun check_file_exists {context = ctxt, ...} txt = |
135 (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) |
137 (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) |
136 then output ctxt [href_link txt] |
138 then output ctxt [href_link txt] |
137 else error (implode ["Source file ", quote txt, " does not exist."])) |
139 else error (implode ["Source file ", quote txt, " does not exist."])) |
138 |
140 |
139 val _ = Thy_Output.antiquotation @{binding "ML_file"} single_arg check_file_exists |
141 val ml_file_setup = Thy_Output.antiquotation @{binding "ML_file"} single_arg check_file_exists |
140 |
142 |
141 |
143 |
142 (* replaces the official subgoal antiquotation with one *) |
144 (* replaces the official subgoal antiquotation with one *) |
143 (* that is closer to the actual output *) |
145 (* that is closer to the actual output *) |
144 fun proof_state state = |
146 fun proof_state state = |
174 val _ = tracing (Pretty.string_of (Pretty.str (Syntax.string_of_term ctxt (prop_of goals)))) |
176 val _ = tracing (Pretty.string_of (Pretty.str (Syntax.string_of_term ctxt (prop_of goals)))) |
175 in |
177 in |
176 Thy_Output.output ctxt output |
178 Thy_Output.output ctxt output |
177 end |
179 end |
178 |
180 |
179 val _ = Thy_Output.antiquotation @{binding "subgoals"} (Scan.succeed ()) output_goals |
181 val subgoals_setup = |
180 val _ = Thy_Output.antiquotation @{binding "raw_goal_state"} (Scan.succeed ()) output_raw_goal_state |
182 Thy_Output.antiquotation @{binding "subgoals"} (Scan.succeed ()) output_goals |
|
183 val raw_goal_state_setup = |
|
184 Thy_Output.antiquotation @{binding "raw_goal_state"} (Scan.succeed ()) output_raw_goal_state |
|
185 |
|
186 val setup = |
|
187 ml_setup #> |
|
188 ml_response_setup #> |
|
189 ml_file_setup #> |
|
190 subgoals_setup #> |
|
191 raw_goal_state_setup |
181 |
192 |
182 end; |
193 end; |