102 (Keyword.tag "TutorialML" Keyword.thy_decl) |
102 (Keyword.tag "TutorialML" Keyword.thy_decl) |
103 (Parse.position Parse.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_text 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 ML {* |
110 val _ = |
111 val _ = |
111 Outer_Syntax.command "ML_prf" "ML text within proof" |
112 Outer_Syntax.command "ML_prf" "ML text within proof" |
112 (Keyword.tag "TutorialML" Keyword.prf_decl) |
113 (Keyword.tag "TutorialML" Keyword.prf_decl) |
113 (Parse.ML_source >> (fn (txt, pos) => |
114 (Parse.ML_source >> (fn (txt, pos) => |
114 Toplevel.proof (Proof.map_context (Context.proof_map |
115 Toplevel.proof (Proof.map_context (Context.proof_map |
115 (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> propagate_env_prf))) |
116 (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> propagate_env_prf))) |
|
117 *} |
116 |
118 |
|
119 ML {* |
117 val _ = |
120 val _ = |
118 Outer_Syntax.command "ML_val" "diagnostic ML text" |
121 Outer_Syntax.command "ML_val" "diagnostic ML text" |
119 (Keyword.tag "TutorialML" Keyword.diag) |
122 (Keyword.tag "TutorialML" Keyword.diag) |
120 (Parse.ML_source >> IsarCmd.ml_diag true) |
123 (Parse.ML_source >> Isar_Cmd.ml_diag true) |
121 *} |
124 *} |
122 |
125 |
123 ML {* |
126 ML {* |
124 val _ = |
127 val _ = |
125 Outer_Syntax.command "setup" "ML theory setup" |
128 Outer_Syntax.command "setup" "ML theory setup" |
126 (Keyword.tag_ml Keyword.thy_decl) |
129 (Keyword.tag_ml Keyword.thy_decl) |
127 (Parse.ML_source >> (fn (txt, pos) => |
130 (Parse.ML_source >> (fn (txt, pos) => |
128 (Toplevel.theory (IsarCmd.global_setup (txt, pos) #> write_file_setup_blk txt)))) |
131 (Toplevel.theory (Isar_Cmd.global_setup (txt, pos) #> write_file_setup_blk txt)))) |
129 *} |
132 *} |
130 |
133 |
131 ML {* |
134 ML {* |
132 val _ = |
135 val _ = |
133 Outer_Syntax.local_theory "local_setup" "ML local theory setup" |
136 Outer_Syntax.local_theory "local_setup" "ML local theory setup" |
134 (Keyword.tag_ml Keyword.thy_decl) |
137 (Keyword.tag_ml Keyword.thy_decl) |
135 (Parse.ML_source >> (fn (txt, pos) => |
138 (Parse.ML_source >> (fn (txt, pos) => |
136 IsarCmd.local_setup (txt, pos) #> write_file_lsetup_blk txt)); |
139 Isar_Cmd.local_setup (txt, pos) #> write_file_lsetup_blk txt)); |
137 *} |
140 *} |
138 |
141 |
139 ML {* |
142 ML {* |
140 fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n) |
143 fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n) |
141 |
144 |