29 (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit |
29 (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit |
30 val value_antiq: string -> |
30 val value_antiq: string -> |
31 (Context.generic * Args.T list -> (string * string) * (Context.generic * Args.T list)) -> unit |
31 (Context.generic * Args.T list -> (string * string) * (Context.generic * Args.T list)) -> unit |
32 val proj_value_antiq: string -> (Context.generic * Args.T list -> |
32 val proj_value_antiq: string -> (Context.generic * Args.T list -> |
33 (string * string * string) * (Context.generic * Args.T list)) -> unit |
33 (string * string * string) * (Context.generic * Args.T list)) -> unit |
34 val eval_antiquotes_fn: (string -> string * string) ref (* FIXME tmp *) |
34 val eval_antiquotes_fn: (string * Position.T -> string * string) ref (* FIXME tmp *) |
35 val trace: bool ref |
35 val trace: bool ref |
36 val use_mltext: string -> bool -> Context.generic option -> unit |
36 val use_mltext: bool -> Position.T -> string -> Context.generic option -> unit |
37 val use_mltext_update: string -> bool -> Context.generic -> Context.generic |
37 val use_mltext_update: bool -> Position.T -> string -> Context.generic -> Context.generic |
38 val use_let: string -> string -> string -> Context.generic -> Context.generic |
38 val use_let: Position.T -> string -> string -> string -> Context.generic -> Context.generic |
39 val use: Path.T -> unit |
39 val use: Path.T -> unit |
40 val evaluate: (string -> unit) * (string -> 'b) -> bool -> |
40 val evaluate: (string -> unit) * (string -> 'b) -> bool -> |
41 string * (unit -> 'a) option ref -> string -> 'a |
41 string * (unit -> 'a) option ref -> string -> 'a |
42 end |
42 end |
43 |
43 |
139 local |
139 local |
140 |
140 |
141 val isabelle_struct = enclose "structure Isabelle =\nstruct\n" "end;"; |
141 val isabelle_struct = enclose "structure Isabelle =\nstruct\n" "end;"; |
142 val isabelle_struct0 = isabelle_struct ""; |
142 val isabelle_struct0 = isabelle_struct ""; |
143 |
143 |
144 fun eval_antiquotes txt = |
144 fun eval_antiquotes txt_pos = |
145 let |
145 let |
146 val ants = Antiquote.scan_antiquotes (txt, Position.line 1); |
146 val ants = Antiquote.scan_antiquotes txt_pos; |
147 |
147 |
148 fun expand (Antiquote.Text s) names = (("", Symbol.escape s), names) |
148 fun expand (Antiquote.Text s) names = (("", Symbol.escape s), names) |
149 | expand (Antiquote.Antiq x) names = |
149 | expand (Antiquote.Antiq x) names = |
150 (case command (Antiquote.scan_arguments (! global_lexicon) antiq x) of |
150 (case command (Antiquote.scan_arguments (! global_lexicon) antiq x) of |
151 Inline s => (("", s), names) |
151 Inline s => (("", s), names) |
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 pr verbose txt = |
173 fun eval_wrapper pr verbose pos txt = |
174 let |
174 let |
175 val (txt1, txt2) = ! eval_antiquotes_fn txt; (* FIXME tmp hook *) |
175 val (txt1, txt2) = ! eval_antiquotes_fn (txt, pos); (* 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 fun eval p = |
|
178 use_text (the_default 1 (Position.line_of p), the_default "ML" (Position.file_of p)) pr; |
178 in |
179 in |
179 NAMED_CRITICAL "ML" (fn () => |
180 NAMED_CRITICAL "ML" (fn () => |
180 (eval "" false txt1; eval name verbose txt2; eval "" false isabelle_struct0)) |
181 (eval Position.none false txt1; |
|
182 eval pos verbose txt2; |
|
183 eval Position.none false isabelle_struct0)) |
181 end; |
184 end; |
182 |
185 |
183 fun ML_wrapper pr = eval_wrapper "ML" pr; |
|
184 |
|
185 end; |
186 end; |
186 |
187 |
187 |
188 |
188 (* ML evaluation *) |
189 (* ML evaluation *) |
189 |
190 |
190 fun use_mltext txt verbose opt_context = |
191 fun use_mltext verbose pos txt opt_context = |
191 setmp opt_context (fn () => ML_wrapper Output.ml_output verbose txt) (); |
192 setmp opt_context (fn () => eval_wrapper Output.ml_output verbose pos txt) (); |
192 |
193 |
193 fun use_mltext_update txt verbose context = |
194 fun use_mltext_update verbose pos txt context = |
194 #2 (pass_context context (fn () => ML_wrapper Output.ml_output verbose txt) ()); |
195 #2 (pass_context context (fn () => eval_wrapper Output.ml_output verbose pos txt) ()); |
195 |
196 |
196 fun use_context txt = use_mltext_update |
197 fun use_let pos bind body txt = |
197 ("ML_Context.set_context (SOME ((" ^ txt ^ ") (ML_Context.the_generic_context ())));") false; |
198 use_mltext_update false pos |
198 |
199 ("ML_Context.set_context (SOME (let " ^ bind ^ " = " ^ txt ^ " in " ^ body ^ |
199 fun use_let bind body txt = |
200 " end (ML_Context.the_generic_context ())));"); |
200 use_context ("let " ^ bind ^ " = " ^ txt ^ " in\n" ^ body ^ " end"); |
201 |
201 |
202 fun use path = eval_wrapper Output.ml_output true (Position.path path) (File.read path); |
202 fun use path = eval_wrapper (Path.implode path) Output.ml_output true (File.read path); |
|
203 |
203 |
204 fun evaluate pr verbose (ref_name, r) txt = NAMED_CRITICAL "ML" (fn () => |
204 fun evaluate pr verbose (ref_name, r) txt = NAMED_CRITICAL "ML" (fn () => |
205 let |
205 let |
206 val _ = r := NONE; |
206 val _ = r := NONE; |
207 val _ = ML_wrapper pr verbose ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))"); |
207 val _ = eval_wrapper pr verbose Position.none |
|
208 ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))"); |
208 in (case ! r of NONE => error ("Bad evaluation for " ^ ref_name) | SOME e => e) end) (); |
209 in (case ! r of NONE => error ("Bad evaluation for " ^ ref_name) | SOME e => e) end) (); |
209 |
210 |
210 |
211 |
211 (* basic antiquotations *) |
212 (* basic antiquotations *) |
212 |
213 |
213 local |
|
214 |
|
215 fun context x = (Scan.state >> Context.proof_of) x; |
214 fun context x = (Scan.state >> Context.proof_of) x; |
|
215 |
|
216 local |
216 |
217 |
217 val _ = value_antiq "context" (Scan.succeed ("context", "ML_Context.the_local_context ()")); |
218 val _ = value_antiq "context" (Scan.succeed ("context", "ML_Context.the_local_context ()")); |
218 |
219 |
219 val _ = inline_antiq "sort" (context -- Scan.lift Args.name >> (fn (ctxt, s) => |
220 val _ = inline_antiq "sort" (context -- Scan.lift Args.name >> (fn (ctxt, s) => |
220 ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))); |
221 ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))); |
241 |> ML_Syntax.print_string)); |
242 |> ML_Syntax.print_string)); |
242 |
243 |
243 val _ = inline_antiq "type_name" (type_ false); |
244 val _ = inline_antiq "type_name" (type_ false); |
244 val _ = inline_antiq "type_syntax" (type_ true); |
245 val _ = inline_antiq "type_syntax" (type_ true); |
245 |
246 |
246 fun const syn = (Scan.state >> Context.proof_of) -- Scan.lift Args.name >> (fn (ctxt, c) => |
247 fun const syn = context -- Scan.lift Args.name >> (fn (ctxt, c) => |
247 #1 (Term.dest_Const (ProofContext.read_const_proper ctxt c)) |
248 #1 (Term.dest_Const (ProofContext.read_const_proper ctxt c)) |
248 |> syn ? ProofContext.const_syntax_name ctxt |
249 |> syn ? ProofContext.const_syntax_name ctxt |
249 |> ML_Syntax.print_string); |
250 |> ML_Syntax.print_string); |
250 |
251 |
251 val _ = inline_antiq "const_name" (const false); |
252 val _ = inline_antiq "const_name" (const false); |
252 val _ = inline_antiq "const_syntax" (const true); |
253 val _ = inline_antiq "const_syntax" (const true); |
253 |
254 |
254 val _ = inline_antiq "const" |
255 val _ = inline_antiq "const" |
255 ((Scan.state >> Context.proof_of) -- Scan.lift Args.name -- |
256 (context -- Scan.lift Args.name -- |
256 Scan.optional (Scan.lift (Args.$$$ "(") |-- Args.enum1 "," Args.typ --| Scan.lift (Args.$$$ ")")) [] |
257 Scan.optional (Scan.lift (Args.$$$ "(") |-- Args.enum1 "," Args.typ --| Scan.lift (Args.$$$ ")")) [] |
257 >> (fn ((ctxt, c), Ts) => |
258 >> (fn ((ctxt, c), Ts) => |
258 let |
259 let |
259 val (c, _) = Term.dest_Const (ProofContext.read_const_proper ctxt c); |
260 val (c, _) = Term.dest_Const (ProofContext.read_const_proper ctxt c); |
260 in ML_Syntax.atomic (ML_Syntax.print_term (ProofContext.mk_const ctxt (c, Ts))) end)); |
261 in ML_Syntax.atomic (ML_Syntax.print_term (ProofContext.mk_const ctxt (c, Ts))) end)); |
274 "Facts.FromTo " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int arg |
275 "Facts.FromTo " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int arg |
275 | print_interval (Facts.From i) = "Facts.From " ^ ML_Syntax.print_int i |
276 | print_interval (Facts.From i) = "Facts.From " ^ ML_Syntax.print_int i |
276 | print_interval (Facts.Single i) = "Facts.Single " ^ ML_Syntax.print_int i; |
277 | print_interval (Facts.Single i) = "Facts.Single " ^ ML_Syntax.print_int i; |
277 |
278 |
278 fun thm_antiq kind get get_name = value_antiq kind |
279 fun thm_antiq kind get get_name = value_antiq kind |
279 ((Scan.state >> Context.proof_of) -- |
280 (context -- Scan.lift (Args.position Args.name -- Scan.option Args.thm_sel) |
280 Scan.lift (Args.position Args.name -- Scan.option Args.thm_sel) |
|
281 >> (fn (ctxt, ((name, pos), sel)) => |
281 >> (fn (ctxt, ((name, pos), sel)) => |
282 let |
282 let |
283 val _ = get ctxt (Facts.Named ((name, pos), sel)); |
283 val _ = get ctxt (Facts.Named ((name, pos), sel)); |
284 val txt = |
284 val txt = |
285 "(Facts.Named ((" ^ ML_Syntax.print_string name ^ ", Position.none), " ^ |
285 "(Facts.Named ((" ^ ML_Syntax.print_string name ^ ", Position.none), " ^ |