19 sig |
19 sig |
20 include BASIC_ML_CONTEXT |
20 include BASIC_ML_CONTEXT |
21 val the_generic_context: unit -> Context.generic |
21 val the_generic_context: unit -> Context.generic |
22 val the_global_context: unit -> theory |
22 val the_global_context: unit -> theory |
23 val the_local_context: unit -> Proof.context |
23 val the_local_context: unit -> Proof.context |
24 val pass_context: Context.generic -> ('a -> 'b) -> 'a -> 'b * Context.generic |
24 val exec: (unit -> unit) -> Context.generic -> Context.generic |
25 val stored_thms: thm list ref |
25 val stored_thms: thm list ref |
26 val ml_store_thm: string * thm -> unit |
26 val ml_store_thm: string * thm -> unit |
27 val ml_store_thms: string * thm list -> unit |
27 val ml_store_thms: string * thm list -> unit |
28 val add_keywords: string list -> unit |
28 val add_keywords: string list -> unit |
29 val inline_antiq: string -> |
29 val inline_antiq: string -> |
32 (Context.generic * Args.T list -> (string * string) * (Context.generic * Args.T list)) -> unit |
32 (Context.generic * Args.T list -> (string * string) * (Context.generic * Args.T list)) -> unit |
33 val proj_value_antiq: string -> (Context.generic * Args.T list -> |
33 val proj_value_antiq: string -> (Context.generic * Args.T list -> |
34 (string * string * string) * (Context.generic * Args.T list)) -> unit |
34 (string * string * string) * (Context.generic * Args.T list)) -> unit |
35 val eval_antiquotes_fn: (string * Position.T -> string * string) ref (* FIXME tmp *) |
35 val eval_antiquotes_fn: (string * Position.T -> string * string) ref (* FIXME tmp *) |
36 val trace: bool ref |
36 val trace: bool ref |
37 val use_mltext: bool -> Position.T -> string -> Context.generic option -> unit |
37 val eval: bool -> Position.T -> string -> unit |
38 val use_mltext_update: bool -> Position.T -> string -> Context.generic -> Context.generic |
38 val eval_file: Path.T -> unit |
39 val use_let: Position.T -> string -> string -> string -> Context.generic -> Context.generic |
39 val eval_in: Context.generic option -> bool -> Position.T -> string -> unit |
40 val use: Path.T -> unit |
|
41 val evaluate: (string -> unit) * (string -> 'b) -> bool -> |
40 val evaluate: (string -> unit) * (string -> 'b) -> bool -> |
42 string * (unit -> 'a) option ref -> string -> 'a |
41 string * (unit -> 'a) option ref -> string -> 'a |
|
42 val expression: Position.T -> string -> string -> string -> Context.generic -> Context.generic |
43 end |
43 end |
44 |
44 |
45 structure ML_Context: ML_CONTEXT = |
45 structure ML_Context: ML_CONTEXT = |
46 struct |
46 struct |
47 |
47 |
49 |
49 |
50 val the_generic_context = Context.the_thread_data; |
50 val the_generic_context = Context.the_thread_data; |
51 val the_global_context = Context.theory_of o the_generic_context; |
51 val the_global_context = Context.theory_of o the_generic_context; |
52 val the_local_context = Context.proof_of o the_generic_context; |
52 val the_local_context = Context.proof_of o the_generic_context; |
53 |
53 |
54 fun pass_context context f x = |
54 fun exec (e: unit -> unit) context = |
55 (case Context.setmp_thread_data (SOME context) (fn () => (f x, Context.thread_data ())) () of |
55 (case Context.setmp_thread_data (SOME context) (fn () => (e (); Context.thread_data ())) () of |
56 (y, SOME context') => (y, context') |
56 SOME context' => context' |
57 | (_, NONE) => error "Lost context after evaluation"); |
57 | NONE => error "Missing context after execution"); |
58 |
58 |
59 |
59 |
60 (* theorem bindings *) |
60 (* theorem bindings *) |
61 |
61 |
62 val store_thms = PureThy.smart_store_thms; |
62 val store_thms = PureThy.smart_store_thms; |
198 end; |
198 end; |
199 |
199 |
200 |
200 |
201 (* ML evaluation *) |
201 (* ML evaluation *) |
202 |
202 |
203 fun use_mltext verbose pos txt opt_context = |
203 val eval = eval_wrapper Output.ml_output; |
204 Context.setmp_thread_data opt_context (fn () => eval_wrapper Output.ml_output verbose pos txt) (); |
204 fun eval_file path = eval true (Position.path path) (File.read path); |
205 |
205 |
206 fun use_mltext_update verbose pos txt context = |
206 fun eval_in context verbose pos txt = |
207 #2 (pass_context context (fn () => eval_wrapper Output.ml_output verbose pos txt) ()); |
207 Context.setmp_thread_data context (fn () => eval verbose pos txt) (); |
208 |
|
209 fun use_let pos bind body txt = |
|
210 use_mltext_update false pos |
|
211 ("Context.set_thread_data (SOME (let " ^ bind ^ " = " ^ txt ^ " in " ^ body ^ |
|
212 " end (ML_Context.the_generic_context ())));"); |
|
213 |
|
214 fun use path = eval_wrapper Output.ml_output true (Position.path path) (File.read path); |
|
215 |
208 |
216 fun evaluate pr verbose (ref_name, r) txt = NAMED_CRITICAL "ML" (fn () => |
209 fun evaluate pr verbose (ref_name, r) txt = NAMED_CRITICAL "ML" (fn () => |
217 let |
210 let |
218 val _ = r := NONE; |
211 val _ = r := NONE; |
219 val _ = eval_wrapper pr verbose Position.none |
212 val _ = eval_wrapper pr verbose Position.none |
220 ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))"); |
213 ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))"); |
221 in (case ! r of NONE => error ("Bad evaluation for " ^ ref_name) | SOME e => e) end) (); |
214 in (case ! r of NONE => error ("Bad evaluation for " ^ ref_name) | SOME e => e) end) (); |
|
215 |
|
216 fun expression pos bind body txt = |
|
217 exec (fn () => eval false pos |
|
218 ("Context.set_thread_data (SOME (let " ^ bind ^ " = " ^ txt ^ " in " ^ body ^ |
|
219 " end (ML_Context.the_generic_context ())));")); |
222 |
220 |
223 |
221 |
224 (* basic antiquotations *) |
222 (* basic antiquotations *) |
225 |
223 |
226 fun context x = (Scan.state >> Context.proof_of) x; |
224 fun context x = (Scan.state >> Context.proof_of) x; |