7 begin |
7 begin |
8 |
8 |
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 inherit_env (context as Context.Proof lthy) = |
12 fun propagate_env (context as Context.Proof lthy) = |
13 Context.Proof (LocalTheory.map_contexts (ML_Context.inherit_env context) lthy) |
13 Context.Proof (LocalTheory.map_contexts (ML_Env.inherit context) lthy) |
14 | inherit_env context = context; |
14 | propagate_env context = context; |
15 |
15 |
16 fun inherit_env_prf prf = Proof.map_contexts |
16 fun propagate_env_prf prf = Proof.map_contexts |
17 (Context.proof_map (ML_Context.inherit_env (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) #> inherit_env))); |
24 (ML_Context.exec (fn () => ML_Context.eval true pos txt) #> propagate_env))); |
25 |
|
26 |
25 |
27 val _ = |
26 val _ = |
28 OuterSyntax.command "ML_prf" "ML text within proof" |
27 OuterSyntax.command "ML_prf" "ML text within proof" |
29 (OuterKeyword.tag "TutorialML" OuterKeyword.prf_decl) |
28 (OuterKeyword.tag "TutorialML" OuterKeyword.prf_decl) |
30 (OuterParse.ML_source >> (fn (txt, pos) => |
29 (OuterParse.ML_source >> (fn (txt, pos) => |
31 Toplevel.proof (Proof.map_context (Context.proof_map |
30 Toplevel.proof (Proof.map_context (Context.proof_map |
32 (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> inherit_env_prf))) |
31 (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> propagate_env_prf))) |
33 |
32 |
34 val _ = |
33 val _ = |
35 OuterSyntax.command "ML_val" "diagnostic ML text" |
34 OuterSyntax.command "ML_val" "diagnostic ML text" |
36 (OuterKeyword.tag "TutorialML" OuterKeyword.diag) |
35 (OuterKeyword.tag "TutorialML" OuterKeyword.diag) |
37 (OuterParse.ML_source >> IsarCmd.ml_diag true); |
36 (OuterParse.ML_source >> IsarCmd.ml_diag true); |