9 (* to have a special tag for text enclosed in ML *) |
9 (* to have a special tag for text enclosed in ML *) |
10 ML {* |
10 ML {* |
11 |
11 |
12 fun propagate_env (context as Context.Proof lthy) = |
12 fun propagate_env (context as Context.Proof lthy) = |
13 Context.Proof (LocalTheory.map_contexts (ML_Env.inherit context) lthy) |
13 Context.Proof (LocalTheory.map_contexts (ML_Env.inherit context) lthy) |
14 | propagate_env context = context; |
14 | propagate_env context = context |
15 |
15 |
16 fun propagate_env_prf prf = Proof.map_contexts |
16 fun propagate_env_prf prf = Proof.map_contexts |
17 (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf; |
17 (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf |
18 |
18 |
19 val _ = |
19 val _ = |
20 OuterSyntax.command "ML" "eval ML text within theory" |
20 OuterSyntax.command "ML" "eval ML text within theory" |
21 (OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl) |
21 (OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl) |
22 (OuterParse.ML_source >> (fn (txt, pos) => |
22 (OuterParse.ML_source >> (fn (txt, pos) => |
23 Toplevel.generic_theory |
23 Toplevel.generic_theory |
24 (ML_Context.exec (fn () => ML_Context.eval true pos txt) #> propagate_env))); |
24 (ML_Context.exec (fn () => ML_Context.eval true pos txt) #> propagate_env))) |
25 |
25 |
26 val _ = |
26 val _ = |
27 OuterSyntax.command "ML_prf" "ML text within proof" |
27 OuterSyntax.command "ML_prf" "ML text within proof" |
28 (OuterKeyword.tag "TutorialML" OuterKeyword.prf_decl) |
28 (OuterKeyword.tag "TutorialML" OuterKeyword.prf_decl) |
29 (OuterParse.ML_source >> (fn (txt, pos) => |
29 (OuterParse.ML_source >> (fn (txt, pos) => |