43 |
43 |
44 fun open_file_prelude name txt = |
44 fun open_file_prelude name txt = |
45 (open_file name; write_file (txt ^ "\n")) |
45 (open_file name; write_file (txt ^ "\n")) |
46 *} |
46 *} |
47 |
47 |
48 |
|
49 ML {* |
48 ML {* |
50 |
49 |
51 fun propagate_env (context as Context.Proof lthy) = |
50 fun propagate_env (context as Context.Proof lthy) = |
52 Context.Proof (LocalTheory.map_contexts (ML_Env.inherit context) lthy) |
51 Context.Proof (LocalTheory.map_contexts (ML_Env.inherit context) lthy) |
53 | propagate_env context = context |
52 | propagate_env context = context |
54 |
53 |
55 fun propagate_env_prf prf = Proof.map_contexts |
54 fun propagate_env_prf prf = Proof.map_contexts |
56 (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf |
55 (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf |
57 *} |
|
58 |
56 |
59 ML {* |
|
60 val _ = |
57 val _ = |
61 OuterSyntax.command "ML" "eval ML text within theory" |
58 OuterSyntax.command "ML" "eval ML text within theory" |
62 (OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl) |
59 (OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl) |
63 (OuterParse.position OuterParse.text >> (fn (txt, pos) => |
60 (OuterParse.position OuterParse.text >> (fn (txt, pos) => |
64 Toplevel.generic_theory |
61 Toplevel.generic_theory |
65 (ML_Context.exec (fn () => (write_file_blk txt; ML_Context.eval true pos txt)) #> propagate_env))) |
62 (ML_Context.exec (fn () => (write_file_blk txt; ML_Context.eval true pos txt)) #> propagate_env))) |
66 *} |
|
67 |
63 |
68 ML {* |
|
69 val _ = |
64 val _ = |
70 OuterSyntax.command "ML_prf" "ML text within proof" |
65 OuterSyntax.command "ML_prf" "ML text within proof" |
71 (OuterKeyword.tag "TutorialML" OuterKeyword.prf_decl) |
66 (OuterKeyword.tag "TutorialML" OuterKeyword.prf_decl) |
72 (OuterParse.ML_source >> (fn (txt, pos) => |
67 (OuterParse.ML_source >> (fn (txt, pos) => |
73 Toplevel.proof (Proof.map_context (Context.proof_map |
68 Toplevel.proof (Proof.map_context (Context.proof_map |
74 (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> propagate_env_prf))) |
69 (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> propagate_env_prf))) |
75 *} |
|
76 |
70 |
77 ML {* |
|
78 val _ = |
71 val _ = |
79 OuterSyntax.command "ML_val" "diagnostic ML text" |
72 OuterSyntax.command "ML_val" "diagnostic ML text" |
80 (OuterKeyword.tag "TutorialML" OuterKeyword.diag) |
73 (OuterKeyword.tag "TutorialML" OuterKeyword.diag) |
81 (OuterParse.ML_source >> IsarCmd.ml_diag true) |
74 (OuterParse.ML_source >> IsarCmd.ml_diag true) |
82 |
75 |