equal
deleted
inserted
replaced
142 \<close> |
142 \<close> |
143 |
143 |
144 setup -- "document antiquotation" |
144 setup -- "document antiquotation" |
145 \<open> |
145 \<open> |
146 Thy_Output.antiquotation @{binding ML_cartouche} |
146 Thy_Output.antiquotation @{binding ML_cartouche} |
147 (Scan.lift Args.cartouche_source_position) (fn {context, ...} => fn source => |
147 (Scan.lift Args.cartouche_input) (fn {context, ...} => fn source => |
148 let |
148 let |
149 val toks = ML_Lex.read "fn _ => (" @ ML_Lex.read_source false source @ ML_Lex.read ");"; |
149 val toks = ML_Lex.read "fn _ => (" @ ML_Lex.read_source false source @ ML_Lex.read ");"; |
150 val _ = ML_Context.eval_in (SOME context) ML_Compiler.flags (Input.pos_of source) toks; |
150 val _ = ML_Context.eval_in (SOME context) ML_Compiler.flags (Input.pos_of source) toks; |
151 in "" end); |
151 in "" end); |
152 \<close> |
152 \<close> |
177 subsubsection \<open>Uniform nesting of sub-languages: document source, ML, term, string literals\<close> |
177 subsubsection \<open>Uniform nesting of sub-languages: document source, ML, term, string literals\<close> |
178 |
178 |
179 ML \<open> |
179 ML \<open> |
180 Outer_Syntax.command |
180 Outer_Syntax.command |
181 @{command_spec "text_cartouche"} "" |
181 @{command_spec "text_cartouche"} "" |
182 (Parse.opt_target -- Parse.source_position Parse.cartouche >> Thy_Output.document_command) |
182 (Parse.opt_target -- Parse.input Parse.cartouche >> Thy_Output.document_command) |
183 \<close> |
183 \<close> |
184 |
184 |
185 text_cartouche |
185 text_cartouche |
186 \<open> |
186 \<open> |
187 @{ML_cartouche |
187 @{ML_cartouche |
223 |
223 |
224 |
224 |
225 subsubsection \<open>Explicit version: method with cartouche argument\<close> |
225 subsubsection \<open>Explicit version: method with cartouche argument\<close> |
226 |
226 |
227 method_setup ml_tactic = \<open> |
227 method_setup ml_tactic = \<open> |
228 Scan.lift Args.cartouche_source_position |
228 Scan.lift Args.cartouche_input |
229 >> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt)) |
229 >> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt)) |
230 \<close> |
230 \<close> |
231 |
231 |
232 lemma "A \<and> B \<longrightarrow> B \<and> A" |
232 lemma "A \<and> B \<longrightarrow> B \<and> A" |
233 apply (ml_tactic \<open>rtac @{thm impI} 1\<close>) |
233 apply (ml_tactic \<open>rtac @{thm impI} 1\<close>) |
244 |
244 |
245 |
245 |
246 subsubsection \<open>Implicit version: method with special name "cartouche" (dynamic!)\<close> |
246 subsubsection \<open>Implicit version: method with special name "cartouche" (dynamic!)\<close> |
247 |
247 |
248 method_setup "cartouche" = \<open> |
248 method_setup "cartouche" = \<open> |
249 Scan.lift Args.cartouche_source_position |
249 Scan.lift Args.cartouche_input |
250 >> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt)) |
250 >> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt)) |
251 \<close> |
251 \<close> |
252 |
252 |
253 lemma "A \<and> B \<longrightarrow> B \<and> A" |
253 lemma "A \<and> B \<longrightarrow> B \<and> A" |
254 apply \<open>rtac @{thm impI} 1\<close> |
254 apply \<open>rtac @{thm impI} 1\<close> |