equal
deleted
inserted
replaced
6 begin |
6 begin |
7 |
7 |
8 (* to have a special tag for text enclosed in ML *) |
8 (* to have a special tag for text enclosed in ML *) |
9 ML {* |
9 ML {* |
10 |
10 |
|
11 fun inherit_env (context as Context.Proof lthy) = |
|
12 Context.Proof (LocalTheory.map_contexts (ML_Context.inherit_env context) lthy) |
|
13 | inherit_env context = context; |
|
14 |
|
15 fun inherit_env_prf prf = Proof.map_contexts |
|
16 (Context.proof_map (ML_Context.inherit_env (Context.Proof (Proof.context_of prf)))) prf |
|
17 |
11 val _ = |
18 val _ = |
12 OuterSyntax.command "ML" "eval ML text within theory" |
19 OuterSyntax.command "ML" "eval ML text within theory" |
13 (OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl) |
20 (OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl) |
14 (OuterParse.ML_source >> (fn (txt, pos) => |
21 (OuterParse.ML_source >> (fn (txt, pos) => |
15 Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt)))); |
22 Toplevel.generic_theory |
|
23 (ML_Context.exec (fn () => ML_Context.eval true pos txt) #> inherit_env))); |
|
24 |
|
25 |
|
26 val _ = |
|
27 OuterSyntax.command "ML_prf" "ML text within proof" |
|
28 (OuterKeyword.tag "TutorialML" OuterKeyword.prf_decl) |
|
29 (OuterParse.ML_source >> (fn (txt, pos) => |
|
30 Toplevel.proof (Proof.map_context (Context.proof_map |
|
31 (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> inherit_env_prf))) |
|
32 |
16 *} |
33 *} |
17 (* |
34 (* |
18 ML {* |
35 ML {* |
19 fun warning str = str |
36 fun warning str = str |
20 fun tracing str = str |
37 fun tracing str = str |