8 signature BASIC_ML_CONTEXT = |
8 signature BASIC_ML_CONTEXT = |
9 sig |
9 sig |
10 val the_context: unit -> theory |
10 val the_context: unit -> theory |
11 val thm: xstring -> thm |
11 val thm: xstring -> thm |
12 val thms: xstring -> thm list |
12 val thms: xstring -> thm list |
13 end; |
13 end |
14 |
14 |
15 signature ML_CONTEXT = |
15 signature ML_CONTEXT = |
16 sig |
16 sig |
17 include BASIC_ML_CONTEXT |
17 include BASIC_ML_CONTEXT |
18 val get_context: unit -> Context.generic option |
18 val get_context: unit -> Context.generic option |
35 val trace: bool ref |
35 val trace: bool ref |
36 val use_mltext: string -> bool -> Context.generic option -> unit |
36 val use_mltext: string -> bool -> Context.generic option -> unit |
37 val use_mltext_update: string -> bool -> Context.generic -> Context.generic |
37 val use_mltext_update: string -> bool -> Context.generic -> Context.generic |
38 val use_let: string -> string -> string -> Context.generic -> Context.generic |
38 val use_let: string -> string -> string -> Context.generic -> Context.generic |
39 val use: Path.T -> unit |
39 val use: Path.T -> unit |
40 end; |
40 val evaluate: (string -> unit) * (string -> 'b) -> bool -> |
|
41 string * (unit -> 'a) option ref -> string -> 'a |
|
42 end |
41 |
43 |
42 structure ML_Context: ML_CONTEXT = |
44 structure ML_Context: ML_CONTEXT = |
43 struct |
45 struct |
44 |
46 |
45 (** Implicit ML context **) |
47 (** Implicit ML context **) |
160 val (decls, body) = |
162 val (decls, body) = |
161 fold_map expand ants ML_Syntax.reserved |
163 fold_map expand ants ML_Syntax.reserved |
162 |> #1 |> split_list |> pairself implode; |
164 |> #1 |> split_list |> pairself implode; |
163 in (isabelle_struct decls, body) end); |
165 in (isabelle_struct decls, body) end); |
164 |
166 |
165 fun eval name verbose txt = use_text name Output.ml_output verbose txt; |
|
166 |
|
167 in |
167 in |
168 |
168 |
169 val eval_antiquotes_fn = ref eval_antiquotes; |
169 val eval_antiquotes_fn = ref eval_antiquotes; |
170 |
170 |
171 val trace = ref false; |
171 val trace = ref false; |
172 |
172 |
173 fun eval_wrapper name verbose txt = |
173 fun eval_wrapper name pr verbose txt = |
174 let |
174 let |
175 val (txt1, txt2) = ! eval_antiquotes_fn txt; |
175 val (txt1, txt2) = ! eval_antiquotes_fn txt; (* FIXME tmp hook *) |
176 val _ = if ! trace then tracing (cat_lines [txt1, txt2]) else (); |
176 val _ = if ! trace then tracing (cat_lines [txt1, txt2]) else (); |
|
177 fun eval nm = use_text nm pr; |
177 in eval "" false txt1; eval name verbose txt2; eval "" false isabelle_struct0 end; |
178 in eval "" false txt1; eval name verbose txt2; eval "" false isabelle_struct0 end; |
178 |
179 |
|
180 fun ML_wrapper pr = eval_wrapper "ML" pr; |
|
181 |
179 end; |
182 end; |
180 |
183 |
181 |
184 |
182 (* ML evaluation *) |
185 (* ML evaluation *) |
183 |
186 |
184 fun use_mltext txt verbose opt_context = |
187 fun use_mltext txt verbose opt_context = |
185 setmp opt_context (fn () => eval_wrapper "ML" verbose txt) (); |
188 setmp opt_context (fn () => ML_wrapper Output.ml_output verbose txt) (); |
186 |
189 |
187 fun use_mltext_update txt verbose context = |
190 fun use_mltext_update txt verbose context = |
188 #2 (pass_context context (eval_wrapper "ML" verbose) txt); |
191 #2 (pass_context context (ML_wrapper Output.ml_output verbose) txt); |
189 |
192 |
190 fun use_context txt = use_mltext_update |
193 fun use_context txt = use_mltext_update |
191 ("ML_Context.set_context (SOME ((" ^ txt ^ ") (ML_Context.the_generic_context ())));") false; |
194 ("ML_Context.set_context (SOME ((" ^ txt ^ ") (ML_Context.the_generic_context ())));") false; |
192 |
195 |
193 fun use_let bind body txt = |
196 fun use_let bind body txt = |
194 use_context ("let " ^ bind ^ " = " ^ txt ^ " in\n" ^ body ^ " end"); |
197 use_context ("let " ^ bind ^ " = " ^ txt ^ " in\n" ^ body ^ " end"); |
195 |
198 |
196 fun use path = eval_wrapper (Path.implode path) true (File.read path); |
199 fun use path = eval_wrapper (Path.implode path) Output.ml_output true (File.read path); |
|
200 |
|
201 fun evaluate pr verbose (ref_name, r) txt = CRITICAL (fn () => |
|
202 let |
|
203 val _ = r := NONE; |
|
204 val _ = ML_wrapper pr verbose ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))"); |
|
205 in (case ! r of NONE => error ("Bad evaluation for " ^ ref_name) | SOME e => e) end) (); |
197 |
206 |
198 |
207 |
199 (* basic antiquotations *) |
208 (* basic antiquotations *) |
200 |
209 |
201 local |
210 local |