83 thy' |
83 thy' |
84 end |
84 end |
85 *} |
85 *} |
86 |
86 |
87 ML {* |
87 ML {* |
88 fun propagate_env (context as Context.Proof lthy) = |
88 val _ = |
89 Context.Proof (Local_Theory.map_contexts (ML_Env.inherit context) lthy) |
89 Outer_Syntax.command ("ML", Keyword.tag "TutorialML" Keyword.thy_decl) |
90 | propagate_env context = context |
90 "ML text within theory or local theory" |
91 |
91 (Parse.ML_source >> (fn (txt, pos) => |
92 fun propagate_env_prf prf = Proof.map_contexts |
92 Toplevel.generic_theory |
93 (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf |
93 (ML_Context.exec (fn () => ML_Context.eval_text true pos txt) #> |
|
94 Local_Theory.propagate_ml_env #> Context.map_theory (write_file_ml_blk txt)))) |
94 *} |
95 *} |
95 |
96 |
96 ML {* |
97 ML {* |
97 val _ = |
98 val _ = |
98 Outer_Syntax.command ("ML", Keyword.tag "TutorialML" Keyword.thy_decl) "eval ML text within theory" |
99 Outer_Syntax.command ("ML_prf", Keyword.tag "TutorialMLprf" Keyword.prf_decl) "ML text within proof" |
99 (Parse.position Parse.text >> |
100 (Parse.ML_source >> (fn (txt, pos) => |
100 (fn (txt, pos) => |
101 Toplevel.proof (Proof.map_context (Context.proof_map |
101 Toplevel.generic_theory |
102 (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> Proof.propagate_ml_env))); |
102 (ML_Context.exec |
|
103 (fn () => ML_Context.eval_text true pos txt) |
|
104 #> propagate_env #> Context.map_theory (write_file_ml_blk txt)))) |
|
105 *} |
103 *} |
106 |
104 |
107 ML {* |
|
108 val _ = |
|
109 Outer_Syntax.command ("ML_prf", Keyword.tag "TutorialMLprf" Keyword.prf_decl) "ML text within proof" |
|
110 (Parse.ML_source >> (fn (txt, pos) => |
|
111 Toplevel.proof (Proof.map_context (Context.proof_map |
|
112 (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> propagate_env_prf))) |
|
113 *} |
|
114 |
105 |
115 ML {* |
106 ML {* |
116 val _ = |
107 val _ = |
117 Outer_Syntax.command ("ML_val", Keyword.tag "TutorialML" Keyword.diag) "diagnostic ML text" |
108 Outer_Syntax.command ("ML_val", Keyword.tag "TutorialML" Keyword.diag) "diagnostic ML text" |
118 (Parse.ML_source >> Isar_Cmd.ml_diag true) |
109 (Parse.ML_source >> Isar_Cmd.ml_diag true) |