equal
deleted
inserted
replaced
99 Toplevel.generic_theory |
99 Toplevel.generic_theory |
100 (ML_Context.exec |
100 (ML_Context.exec |
101 (fn () => ML_Context.eval_text true pos txt) |
101 (fn () => ML_Context.eval_text true pos txt) |
102 #> propagate_env #> Context.map_theory (write_file_ml_blk txt)))) |
102 #> propagate_env #> Context.map_theory (write_file_ml_blk txt)))) |
103 *} |
103 *} |
|
104 |
104 ML {* |
105 ML {* |
105 val _ = |
106 val _ = |
106 Outer_Syntax.command "ML_prf" "ML text within proof" |
107 Outer_Syntax.command "ML_prf" "ML text within proof" |
107 (Keyword.tag "TutorialML" Keyword.prf_decl) |
108 (Keyword.tag "TutorialMLprf" Keyword.prf_decl) |
108 (Parse.ML_source >> (fn (txt, pos) => |
109 (Parse.ML_source >> (fn (txt, pos) => |
109 Toplevel.proof (Proof.map_context (Context.proof_map |
110 Toplevel.proof (Proof.map_context (Context.proof_map |
110 (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> propagate_env_prf))) |
111 (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> propagate_env_prf))) |
111 *} |
112 *} |
112 |
113 |