96 (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf |
96 (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf |
97 *} |
97 *} |
98 |
98 |
99 ML {* |
99 ML {* |
100 val _ = |
100 val _ = |
101 OuterSyntax.command "ML" "eval ML text within theory" |
101 Outer_Syntax.command "ML" "eval ML text within theory" |
102 (OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl) |
102 (Keyword.tag "TutorialML" Keyword.thy_decl) |
103 (OuterParse.position OuterParse.text >> |
103 (Parse.position Parse.text >> |
104 (fn (txt, pos) => |
104 (fn (txt, pos) => |
105 Toplevel.generic_theory |
105 Toplevel.generic_theory |
106 (ML_Context.exec |
106 (ML_Context.exec |
107 (fn () => ML_Context.eval true pos txt) |
107 (fn () => ML_Context.eval true pos txt) |
108 #> propagate_env #> Context.map_theory (write_file_ml_blk txt)))) |
108 #> propagate_env #> Context.map_theory (write_file_ml_blk txt)))) |
109 |
109 |
110 val _ = |
110 val _ = |
111 OuterSyntax.command "ML_prf" "ML text within proof" |
111 Outer_Syntax.command "ML_prf" "ML text within proof" |
112 (OuterKeyword.tag "TutorialML" OuterKeyword.prf_decl) |
112 (Keyword.tag "TutorialML" Keyword.prf_decl) |
113 (OuterParse.ML_source >> (fn (txt, pos) => |
113 (Parse.ML_source >> (fn (txt, pos) => |
114 Toplevel.proof (Proof.map_context (Context.proof_map |
114 Toplevel.proof (Proof.map_context (Context.proof_map |
115 (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> propagate_env_prf))) |
115 (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> propagate_env_prf))) |
116 |
116 |
117 val _ = |
117 val _ = |
118 OuterSyntax.command "ML_val" "diagnostic ML text" |
118 Outer_Syntax.command "ML_val" "diagnostic ML text" |
119 (OuterKeyword.tag "TutorialML" OuterKeyword.diag) |
119 (Keyword.tag "TutorialML" Keyword.diag) |
120 (OuterParse.ML_source >> IsarCmd.ml_diag true) |
120 (Parse.ML_source >> IsarCmd.ml_diag true) |
121 *} |
121 *} |
122 |
122 |
123 ML {* |
123 ML {* |
124 val _ = |
124 val _ = |
125 OuterSyntax.command "setup" "ML theory setup" |
125 Outer_Syntax.command "setup" "ML theory setup" |
126 (OuterKeyword.tag_ml OuterKeyword.thy_decl) |
126 (Keyword.tag_ml Keyword.thy_decl) |
127 (OuterParse.ML_source >> (fn (txt, pos) => |
127 (Parse.ML_source >> (fn (txt, pos) => |
128 (Toplevel.theory (IsarCmd.global_setup (txt, pos) #> write_file_setup_blk txt)))) |
128 (Toplevel.theory (IsarCmd.global_setup (txt, pos) #> write_file_setup_blk txt)))) |
129 *} |
129 *} |
130 |
130 |
131 ML {* Context.proof_map *} |
|
132 ML {* IsarCmd.local_setup ; Context.map_proof (write_file_lsetup_blk "") *} |
|
133 |
|
134 |
|
135 ML {* |
131 ML {* |
136 val _ = |
132 val _ = |
137 OuterSyntax.local_theory "local_setup" "ML local theory setup" |
133 Outer_Syntax.local_theory "local_setup" "ML local theory setup" |
138 (OuterKeyword.tag_ml OuterKeyword.thy_decl) |
134 (Keyword.tag_ml Keyword.thy_decl) |
139 (OuterParse.ML_source >> (fn (txt, pos) => |
135 (Parse.ML_source >> (fn (txt, pos) => |
140 IsarCmd.local_setup (txt, pos) #> write_file_lsetup_blk txt)); |
136 IsarCmd.local_setup (txt, pos) #> write_file_lsetup_blk txt)); |
141 *} |
137 *} |
142 |
138 |
143 ML {* |
139 ML {* |
144 fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n) |
140 fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n) |