90 (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf |
93 (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf |
91 *} |
94 *} |
92 |
95 |
93 ML {* |
96 ML {* |
94 val _ = |
97 val _ = |
95 Outer_Syntax.command "ML" "eval ML text within theory" |
98 Outer_Syntax.command ("ML", Keyword.tag "TutorialML" Keyword.thy_decl) "eval ML text within theory" |
96 (Keyword.tag "TutorialML" Keyword.thy_decl) |
|
97 (Parse.position Parse.text >> |
99 (Parse.position Parse.text >> |
98 (fn (txt, pos) => |
100 (fn (txt, pos) => |
99 Toplevel.generic_theory |
101 Toplevel.generic_theory |
100 (ML_Context.exec |
102 (ML_Context.exec |
101 (fn () => ML_Context.eval_text true pos txt) |
103 (fn () => ML_Context.eval_text true pos txt) |
102 #> propagate_env #> Context.map_theory (write_file_ml_blk txt)))) |
104 #> propagate_env #> Context.map_theory (write_file_ml_blk txt)))) |
103 *} |
105 *} |
104 |
106 |
105 ML {* |
107 ML {* |
106 val _ = |
108 val _ = |
107 Outer_Syntax.command "ML_prf" "ML text within proof" |
109 Outer_Syntax.command ("ML_prf", Keyword.tag "TutorialMLprf" Keyword.prf_decl) "ML text within proof" |
108 (Keyword.tag "TutorialMLprf" Keyword.prf_decl) |
|
109 (Parse.ML_source >> (fn (txt, pos) => |
110 (Parse.ML_source >> (fn (txt, pos) => |
110 Toplevel.proof (Proof.map_context (Context.proof_map |
111 Toplevel.proof (Proof.map_context (Context.proof_map |
111 (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> propagate_env_prf))) |
112 (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> propagate_env_prf))) |
112 *} |
113 *} |
113 |
114 |
114 ML {* |
115 ML {* |
115 val _ = |
116 val _ = |
116 Outer_Syntax.command "ML_val" "diagnostic ML text" |
117 Outer_Syntax.command ("ML_val", Keyword.tag "TutorialML" Keyword.diag) "diagnostic ML text" |
117 (Keyword.tag "TutorialML" Keyword.diag) |
|
118 (Parse.ML_source >> Isar_Cmd.ml_diag true) |
118 (Parse.ML_source >> Isar_Cmd.ml_diag true) |
119 *} |
119 *} |
120 |
120 |
121 ML {* |
121 ML {* |
122 val _ = |
122 val _ = |
123 Outer_Syntax.command "setup" "ML theory setup" |
123 Outer_Syntax.command ("setup", Keyword.tag_ml Keyword.thy_decl) "ML theory setup" |
124 (Keyword.tag_ml Keyword.thy_decl) |
|
125 (Parse.ML_source >> (fn (txt, pos) => |
124 (Parse.ML_source >> (fn (txt, pos) => |
126 (Toplevel.theory (Isar_Cmd.global_setup (txt, pos) #> write_file_setup_blk txt)))) |
125 (Toplevel.theory (Isar_Cmd.global_setup (txt, pos) #> write_file_setup_blk txt)))) |
127 *} |
126 *} |
128 |
127 |
129 ML {* |
128 ML {* |
130 val _ = |
129 val _ = |
131 Outer_Syntax.local_theory "local_setup" "ML local theory setup" |
130 Outer_Syntax.local_theory ("local_setup", Keyword.tag_ml Keyword.thy_decl) "ML local theory setup" |
132 (Keyword.tag_ml Keyword.thy_decl) |
|
133 (Parse.ML_source >> (fn (txt, pos) => |
131 (Parse.ML_source >> (fn (txt, pos) => |
134 Isar_Cmd.local_setup (txt, pos) #> write_file_lsetup_blk txt)); |
132 Isar_Cmd.local_setup (txt, pos) #> write_file_lsetup_blk txt)); |
135 *} |
133 *} |
136 |
134 |
137 ML {* |
135 ML {* |