270 |
270 |
271 val _ = |
271 val _ = |
272 OuterSyntax.local_theory "lemmas" "define lemmas" K.thy_decl (theorems Thm.lemmaK); |
272 OuterSyntax.local_theory "lemmas" "define lemmas" K.thy_decl (theorems Thm.lemmaK); |
273 |
273 |
274 val _ = |
274 val _ = |
275 OuterSyntax.local_theory "declare" "declare theorems (improper)" K.thy_decl |
275 OuterSyntax.local_theory "declare" "declare theorems" K.thy_decl |
276 (P.and_list1 SpecParse.xthms1 |
276 (P.and_list1 SpecParse.xthms1 |
277 >> (fn args => #2 o Specification.theorems_cmd "" [(Attrib.empty_binding, flat args)])); |
277 >> (fn args => #2 o Specification.theorems_cmd "" [(Attrib.empty_binding, flat args)])); |
278 |
278 |
279 |
279 |
280 (* name space entry path *) |
280 (* name space entry path *) |
293 (Toplevel.theory o uncurry IsarCmd.hide_names)); |
293 (Toplevel.theory o uncurry IsarCmd.hide_names)); |
294 |
294 |
295 |
295 |
296 (* use ML text *) |
296 (* use ML text *) |
297 |
297 |
298 val _ = |
298 fun inherit_env (context as Context.Proof lthy) = |
299 OuterSyntax.command "use" "eval ML text from file" (K.tag_ml K.thy_decl) |
299 Context.Proof (LocalTheory.map_contexts (ML_Context.inherit_env context) lthy) |
300 (P.path >> (Toplevel.generic_theory o ThyInfo.exec_file false)); |
300 | inherit_env context = context; |
301 |
301 |
302 val _ = |
302 fun inherit_env_prf prf = Proof.map_contexts |
303 OuterSyntax.command "ML" "eval ML text within theory" (K.tag_ml K.thy_decl) |
303 (Context.proof_map (ML_Context.inherit_env (Context.Proof (Proof.context_of prf)))) prf; |
|
304 |
|
305 val _ = |
|
306 OuterSyntax.command "use" "ML text from file" (K.tag_ml K.thy_decl) |
|
307 (P.path >> (fn path => Toplevel.generic_theory (ThyInfo.exec_file false path #> inherit_env))); |
|
308 |
|
309 val _ = |
|
310 OuterSyntax.command "ML" "ML text within theory or local theory" (K.tag_ml K.thy_decl) |
304 (P.ML_source >> (fn (txt, pos) => |
311 (P.ML_source >> (fn (txt, pos) => |
305 Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt)))); |
312 Toplevel.generic_theory |
306 |
313 (ML_Context.exec (fn () => ML_Context.eval true pos txt) #> inherit_env))); |
307 val _ = |
314 |
308 OuterSyntax.command "ML_prf" "eval ML text within proof" (K.tag_proof K.prf_decl) |
315 val _ = |
|
316 OuterSyntax.command "ML_prf" "ML text within proof" (K.tag_proof K.prf_decl) |
309 (P.ML_source >> (fn (txt, pos) => |
317 (P.ML_source >> (fn (txt, pos) => |
310 Toplevel.proof (Proof.map_context (Context.proof_map |
318 Toplevel.proof (Proof.map_context (Context.proof_map |
311 (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> |
319 (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> inherit_env_prf))); |
312 (fn prf => prf |> Proof.map_contexts |
320 |
313 (Context.proof_map (ML_Context.inherit_env (Context.Proof (Proof.context_of prf)))))))); |
321 val _ = |
314 |
322 OuterSyntax.command "ML_val" "diagnostic ML text" (K.tag_ml K.diag) |
315 val _ = |
|
316 OuterSyntax.command "ML_val" "eval ML text (diagnostic)" (K.tag_ml K.diag) |
|
317 (P.ML_source >> IsarCmd.ml_diag true); |
323 (P.ML_source >> IsarCmd.ml_diag true); |
318 |
324 |
319 val _ = |
325 val _ = |
320 OuterSyntax.command "ML_command" "silently eval ML text (diagnostic)" (K.tag_ml K.diag) |
326 OuterSyntax.command "ML_command" "diagnostic ML text (silent)" (K.tag_ml K.diag) |
321 (P.ML_source >> (Toplevel.no_timing oo IsarCmd.ml_diag false)); |
327 (P.ML_source >> (Toplevel.no_timing oo IsarCmd.ml_diag false)); |
322 |
328 |
323 val _ = |
329 val _ = |
324 OuterSyntax.command "setup" "ML theory setup" (K.tag_ml K.thy_decl) |
330 OuterSyntax.command "setup" "ML theory setup" (K.tag_ml K.thy_decl) |
325 (P.ML_source >> (Toplevel.theory o IsarCmd.global_setup)); |
331 (P.ML_source >> (Toplevel.theory o IsarCmd.global_setup)); |