author | wenzelm |
Wed, 14 May 2008 11:05:08 +0200 | |
changeset 26881 | bb68f50644a9 |
parent 26658 | 5967c2a0a94f |
child 27343 | 4b28b80dd1f8 |
permissions | -rw-r--r-- |
24581 | 1 |
(* Title: Pure/ML/ml_context.ML |
24574 | 2 |
ID: $Id$ |
3 |
Author: Makarius |
|
4 |
||
5 |
ML context and antiquotations. |
|
6 |
*) |
|
7 |
||
8 |
signature BASIC_ML_CONTEXT = |
|
9 |
sig |
|
26416
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
10 |
val bind_thm: string * thm -> unit |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
11 |
val bind_thms: string * thm list -> unit |
24574 | 12 |
val thm: xstring -> thm |
13 |
val thms: xstring -> thm list |
|
25204 | 14 |
end |
24574 | 15 |
|
16 |
signature ML_CONTEXT = |
|
17 |
sig |
|
18 |
include BASIC_ML_CONTEXT |
|
19 |
val the_generic_context: unit -> Context.generic |
|
26432
095e448b95a0
renamed ML_Context.the_context to ML_Context.the_global_context;
wenzelm
parents:
26416
diff
changeset
|
20 |
val the_global_context: unit -> theory |
24574 | 21 |
val the_local_context: unit -> Proof.context |
26455 | 22 |
val exec: (unit -> unit) -> Context.generic -> Context.generic |
26416
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
23 |
val stored_thms: thm list ref |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
24 |
val ml_store_thm: string * thm -> unit |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
25 |
val ml_store_thms: string * thm list -> unit |
24574 | 26 |
val add_keywords: string list -> unit |
27 |
val inline_antiq: string -> |
|
28 |
(Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit |
|
29 |
val value_antiq: string -> |
|
30 |
(Context.generic * Args.T list -> (string * string) * (Context.generic * Args.T list)) -> unit |
|
31 |
val proj_value_antiq: string -> (Context.generic * Args.T list -> |
|
32 |
(string * string * string) * (Context.generic * Args.T list)) -> unit |
|
33 |
val trace: bool ref |
|
26455 | 34 |
val eval: bool -> Position.T -> string -> unit |
35 |
val eval_file: Path.T -> unit |
|
36 |
val eval_in: Context.generic option -> bool -> Position.T -> string -> unit |
|
25204 | 37 |
val evaluate: (string -> unit) * (string -> 'b) -> bool -> |
38 |
string * (unit -> 'a) option ref -> string -> 'a |
|
26455 | 39 |
val expression: Position.T -> string -> string -> string -> Context.generic -> Context.generic |
25204 | 40 |
end |
24574 | 41 |
|
42 |
structure ML_Context: ML_CONTEXT = |
|
43 |
struct |
|
44 |
||
26416
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
45 |
(** implicit ML context **) |
24574 | 46 |
|
26416
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
47 |
val the_generic_context = Context.the_thread_data; |
26432
095e448b95a0
renamed ML_Context.the_context to ML_Context.the_global_context;
wenzelm
parents:
26416
diff
changeset
|
48 |
val the_global_context = Context.theory_of o the_generic_context; |
24574 | 49 |
val the_local_context = Context.proof_of o the_generic_context; |
50 |
||
26455 | 51 |
fun exec (e: unit -> unit) context = |
52 |
(case Context.setmp_thread_data (SOME context) (fn () => (e (); Context.thread_data ())) () of |
|
53 |
SOME context' => context' |
|
54 |
| NONE => error "Missing context after execution"); |
|
26416
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
55 |
|
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
56 |
|
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
57 |
(* theorem bindings *) |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
58 |
|
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
59 |
val stored_thms: thm list ref = ref []; |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
60 |
|
26492
6e87cc839632
removed obsolete store_thm(s), cf. functional versions in pure_thy.ML;
wenzelm
parents:
26473
diff
changeset
|
61 |
fun ml_store sel (name, ths) = |
6e87cc839632
removed obsolete store_thm(s), cf. functional versions in pure_thy.ML;
wenzelm
parents:
26473
diff
changeset
|
62 |
let |
6e87cc839632
removed obsolete store_thm(s), cf. functional versions in pure_thy.ML;
wenzelm
parents:
26473
diff
changeset
|
63 |
val ths' = Context.>>> (Context.map_theory_result (PureThy.store_thms (name, ths))); |
6e87cc839632
removed obsolete store_thm(s), cf. functional versions in pure_thy.ML;
wenzelm
parents:
26473
diff
changeset
|
64 |
val _ = |
6e87cc839632
removed obsolete store_thm(s), cf. functional versions in pure_thy.ML;
wenzelm
parents:
26473
diff
changeset
|
65 |
if name = "" then () |
6e87cc839632
removed obsolete store_thm(s), cf. functional versions in pure_thy.ML;
wenzelm
parents:
26473
diff
changeset
|
66 |
else if not (ML_Syntax.is_identifier name) then |
6e87cc839632
removed obsolete store_thm(s), cf. functional versions in pure_thy.ML;
wenzelm
parents:
26473
diff
changeset
|
67 |
error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value") |
6e87cc839632
removed obsolete store_thm(s), cf. functional versions in pure_thy.ML;
wenzelm
parents:
26473
diff
changeset
|
68 |
else setmp stored_thms ths' (fn () => |
6e87cc839632
removed obsolete store_thm(s), cf. functional versions in pure_thy.ML;
wenzelm
parents:
26473
diff
changeset
|
69 |
use_text (0, "") Output.ml_output true |
6e87cc839632
removed obsolete store_thm(s), cf. functional versions in pure_thy.ML;
wenzelm
parents:
26473
diff
changeset
|
70 |
("val " ^ name ^ " = " ^ sel ^ "(! ML_Context.stored_thms);")) (); |
6e87cc839632
removed obsolete store_thm(s), cf. functional versions in pure_thy.ML;
wenzelm
parents:
26473
diff
changeset
|
71 |
in () end; |
24574 | 72 |
|
26492
6e87cc839632
removed obsolete store_thm(s), cf. functional versions in pure_thy.ML;
wenzelm
parents:
26473
diff
changeset
|
73 |
val ml_store_thms = ml_store ""; |
6e87cc839632
removed obsolete store_thm(s), cf. functional versions in pure_thy.ML;
wenzelm
parents:
26473
diff
changeset
|
74 |
fun ml_store_thm (name, th) = ml_store "hd" (name, [th]); |
26416
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
75 |
|
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
76 |
fun bind_thm (name, thm) = ml_store_thm (name, Drule.standard thm); |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
77 |
fun bind_thms (name, thms) = ml_store_thms (name, map Drule.standard thms); |
24574 | 78 |
|
79 |
||
80 |
||
81 |
(** ML antiquotations **) |
|
82 |
||
83 |
(* maintain keywords *) |
|
84 |
||
85 |
val global_lexicon = ref Scan.empty_lexicon; |
|
86 |
||
87 |
fun add_keywords keywords = CRITICAL (fn () => |
|
88 |
change global_lexicon (Scan.extend_lexicon (map Symbol.explode keywords))); |
|
89 |
||
90 |
||
91 |
(* maintain commands *) |
|
92 |
||
93 |
datatype antiq = Inline of string | ProjValue of string * string * string; |
|
94 |
val global_parsers = ref (Symtab.empty: |
|
95 |
(Context.generic * Args.T list -> antiq * (Context.generic * Args.T list)) Symtab.table); |
|
96 |
||
97 |
local |
|
98 |
||
99 |
fun add_item kind name scan = CRITICAL (fn () => |
|
100 |
change global_parsers (fn tab => |
|
101 |
(if not (Symtab.defined tab name) then () |
|
102 |
else warning ("Redefined ML antiquotation: " ^ quote name); |
|
103 |
Symtab.update (name, scan >> kind) tab))); |
|
104 |
||
105 |
in |
|
106 |
||
107 |
val inline_antiq = add_item Inline; |
|
108 |
val proj_value_antiq = add_item ProjValue; |
|
109 |
fun value_antiq name scan = proj_value_antiq name (scan >> (fn (a, s) => (a, s, ""))); |
|
110 |
||
111 |
end; |
|
112 |
||
113 |
||
114 |
(* command syntax *) |
|
115 |
||
116 |
fun syntax scan src = |
|
117 |
#1 (Args.context_syntax "ML antiquotation" scan src (the_local_context ())); |
|
118 |
||
119 |
fun command src = |
|
120 |
let val ((name, _), pos) = Args.dest_src src in |
|
121 |
(case Symtab.lookup (! global_parsers) name of |
|
122 |
NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos) |
|
123 |
| SOME scan => syntax scan src) |
|
124 |
end; |
|
125 |
||
126 |
||
127 |
(* outer syntax *) |
|
128 |
||
129 |
structure T = OuterLex; |
|
130 |
structure P = OuterParse; |
|
131 |
||
132 |
val antiq = |
|
133 |
P.!!! (P.position P.xname -- P.arguments --| Scan.ahead P.eof) |
|
134 |
>> (fn ((x, pos), y) => Args.src ((x, y), pos)); |
|
135 |
||
136 |
||
137 |
(* input/output wrappers *) |
|
138 |
||
139 |
local |
|
140 |
||
26473
2266e5fd7b63
eval_wrapper: non-critical version via unique Isabelle structure, proper forget_structure;
wenzelm
parents:
26455
diff
changeset
|
141 |
fun eval_antiquotes struct_name txt_pos = |
24574 | 142 |
let |
26473
2266e5fd7b63
eval_wrapper: non-critical version via unique Isabelle structure, proper forget_structure;
wenzelm
parents:
26455
diff
changeset
|
143 |
val lex = ! global_lexicon; |
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
144 |
val ants = Antiquote.scan_antiquotes txt_pos; |
24574 | 145 |
|
146 |
fun expand (Antiquote.Text s) names = (("", Symbol.escape s), names) |
|
147 |
| expand (Antiquote.Antiq x) names = |
|
26473
2266e5fd7b63
eval_wrapper: non-critical version via unique Isabelle structure, proper forget_structure;
wenzelm
parents:
26455
diff
changeset
|
148 |
(case command (Antiquote.scan_arguments lex antiq x) of |
24574 | 149 |
Inline s => (("", s), names) |
150 |
| ProjValue (a, s, f) => |
|
151 |
let |
|
152 |
val a' = if ML_Syntax.is_identifier a then a else "val"; |
|
153 |
val ([b], names') = Name.variants [a'] names; |
|
154 |
val binding = "val " ^ b ^ " = " ^ s ^ ";\n"; |
|
155 |
val value = |
|
26473
2266e5fd7b63
eval_wrapper: non-critical version via unique Isabelle structure, proper forget_structure;
wenzelm
parents:
26455
diff
changeset
|
156 |
if f = "" then struct_name ^ "." ^ b |
2266e5fd7b63
eval_wrapper: non-critical version via unique Isabelle structure, proper forget_structure;
wenzelm
parents:
26455
diff
changeset
|
157 |
else "(" ^ f ^ " " ^ struct_name ^ "." ^ b ^ ")"; |
24574 | 158 |
in ((binding, value), names') end); |
159 |
||
160 |
val (decls, body) = |
|
26473
2266e5fd7b63
eval_wrapper: non-critical version via unique Isabelle structure, proper forget_structure;
wenzelm
parents:
26455
diff
changeset
|
161 |
fold_map expand ants ML_Syntax.reserved |
24574 | 162 |
|> #1 |> split_list |> pairself implode; |
26473
2266e5fd7b63
eval_wrapper: non-critical version via unique Isabelle structure, proper forget_structure;
wenzelm
parents:
26455
diff
changeset
|
163 |
in ("structure " ^ struct_name ^ " =\nstruct\n" ^ decls ^ "end;", body) end; |
24574 | 164 |
|
165 |
in |
|
166 |
||
167 |
val trace = ref false; |
|
168 |
||
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
169 |
fun eval_wrapper pr verbose pos txt = |
24574 | 170 |
let |
26473
2266e5fd7b63
eval_wrapper: non-critical version via unique Isabelle structure, proper forget_structure;
wenzelm
parents:
26455
diff
changeset
|
171 |
val struct_name = |
2266e5fd7b63
eval_wrapper: non-critical version via unique Isabelle structure, proper forget_structure;
wenzelm
parents:
26455
diff
changeset
|
172 |
if Multithreading.available then "Isabelle" ^ serial_string () |
2266e5fd7b63
eval_wrapper: non-critical version via unique Isabelle structure, proper forget_structure;
wenzelm
parents:
26455
diff
changeset
|
173 |
else "Isabelle"; |
26658 | 174 |
val (txt1, txt2) = eval_antiquotes struct_name (txt, pos); |
24574 | 175 |
val _ = if ! trace then tracing (cat_lines [txt1, txt2]) else (); |
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
176 |
fun eval p = |
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
177 |
use_text (the_default 1 (Position.line_of p), the_default "ML" (Position.file_of p)) pr; |
25755 | 178 |
in |
26473
2266e5fd7b63
eval_wrapper: non-critical version via unique Isabelle structure, proper forget_structure;
wenzelm
parents:
26455
diff
changeset
|
179 |
eval Position.none false txt1; |
26658 | 180 |
NAMED_CRITICAL "ML" (fn () => eval pos verbose txt2); (* FIXME non-critical with local ML env *) |
26473
2266e5fd7b63
eval_wrapper: non-critical version via unique Isabelle structure, proper forget_structure;
wenzelm
parents:
26455
diff
changeset
|
181 |
forget_structure struct_name |
25755 | 182 |
end; |
24574 | 183 |
|
184 |
end; |
|
185 |
||
186 |
||
187 |
(* ML evaluation *) |
|
188 |
||
26455 | 189 |
val eval = eval_wrapper Output.ml_output; |
26881 | 190 |
fun eval_file path = eval true (Path.position path) (File.read path); |
24574 | 191 |
|
26455 | 192 |
fun eval_in context verbose pos txt = |
193 |
Context.setmp_thread_data context (fn () => eval verbose pos txt) (); |
|
25204 | 194 |
|
25700 | 195 |
fun evaluate pr verbose (ref_name, r) txt = NAMED_CRITICAL "ML" (fn () => |
25204 | 196 |
let |
197 |
val _ = r := NONE; |
|
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
198 |
val _ = eval_wrapper pr verbose Position.none |
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
199 |
("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))"); |
25204 | 200 |
in (case ! r of NONE => error ("Bad evaluation for " ^ ref_name) | SOME e => e) end) (); |
24574 | 201 |
|
26455 | 202 |
fun expression pos bind body txt = |
203 |
exec (fn () => eval false pos |
|
204 |
("Context.set_thread_data (SOME (let " ^ bind ^ " = " ^ txt ^ " in " ^ body ^ |
|
205 |
" end (ML_Context.the_generic_context ())));")); |
|
206 |
||
24574 | 207 |
|
208 |
(* basic antiquotations *) |
|
209 |
||
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
210 |
fun context x = (Scan.state >> Context.proof_of) x; |
25142 | 211 |
|
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
212 |
local |
25142 | 213 |
|
24574 | 214 |
val _ = value_antiq "context" (Scan.succeed ("context", "ML_Context.the_local_context ()")); |
215 |
||
25142 | 216 |
val _ = inline_antiq "sort" (context -- Scan.lift Args.name >> (fn (ctxt, s) => |
217 |
ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))); |
|
218 |
||
24574 | 219 |
val _ = inline_antiq "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)); |
220 |
val _ = inline_antiq "term" (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)); |
|
221 |
val _ = inline_antiq "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)); |
|
222 |
||
223 |
val _ = value_antiq "ctyp" (Args.typ >> (fn T => |
|
224 |
("ctyp", |
|
26432
095e448b95a0
renamed ML_Context.the_context to ML_Context.the_global_context;
wenzelm
parents:
26416
diff
changeset
|
225 |
"Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T)))); |
24574 | 226 |
|
227 |
val _ = value_antiq "cterm" (Args.term >> (fn t => |
|
228 |
("cterm", |
|
26432
095e448b95a0
renamed ML_Context.the_context to ML_Context.the_global_context;
wenzelm
parents:
26416
diff
changeset
|
229 |
"Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)))); |
24574 | 230 |
|
231 |
val _ = value_antiq "cprop" (Args.prop >> (fn t => |
|
232 |
("cprop", |
|
26432
095e448b95a0
renamed ML_Context.the_context to ML_Context.the_global_context;
wenzelm
parents:
26416
diff
changeset
|
233 |
"Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)))); |
24574 | 234 |
|
25142 | 235 |
fun type_ syn = (context -- Scan.lift Args.name >> (fn (ctxt, c) => |
24695 | 236 |
#1 (Term.dest_Type (ProofContext.read_tyname ctxt c)) |
25142 | 237 |
|> syn ? Sign.base_name |
24695 | 238 |
|> ML_Syntax.print_string)); |
24574 | 239 |
|
25142 | 240 |
val _ = inline_antiq "type_name" (type_ false); |
241 |
val _ = inline_antiq "type_syntax" (type_ true); |
|
242 |
||
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
243 |
fun const syn = context -- Scan.lift Args.name >> (fn (ctxt, c) => |
25346
7f2e3292e3dd
renamed ProofContext.read_const' to ProofContext.read_const_proper;
wenzelm
parents:
25334
diff
changeset
|
244 |
#1 (Term.dest_Const (ProofContext.read_const_proper ctxt c)) |
24574 | 245 |
|> syn ? ProofContext.const_syntax_name ctxt |
246 |
|> ML_Syntax.print_string); |
|
247 |
||
248 |
val _ = inline_antiq "const_name" (const false); |
|
249 |
val _ = inline_antiq "const_syntax" (const true); |
|
250 |
||
26188 | 251 |
val _ = inline_antiq "const" |
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
252 |
(context -- Scan.lift Args.name -- |
26188 | 253 |
Scan.optional (Scan.lift (Args.$$$ "(") |-- Args.enum1 "," Args.typ --| Scan.lift (Args.$$$ ")")) [] |
254 |
>> (fn ((ctxt, c), Ts) => |
|
26473
2266e5fd7b63
eval_wrapper: non-critical version via unique Isabelle structure, proper forget_structure;
wenzelm
parents:
26455
diff
changeset
|
255 |
let val (c, _) = Term.dest_Const (ProofContext.read_const_proper ctxt c) |
26268 | 256 |
in ML_Syntax.atomic (ML_Syntax.print_term (ProofContext.mk_const ctxt (c, Ts))) end)); |
26188 | 257 |
|
25142 | 258 |
in val _ = () end; |
24574 | 259 |
|
260 |
||
26416
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
261 |
|
24574 | 262 |
(** fact references **) |
263 |
||
26346
17debd2fff8e
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset
|
264 |
fun thm name = ProofContext.get_thm (the_local_context ()) name; |
17debd2fff8e
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset
|
265 |
fun thms name = ProofContext.get_thms (the_local_context ()) name; |
24574 | 266 |
|
267 |
||
268 |
local |
|
269 |
||
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26268
diff
changeset
|
270 |
fun print_interval (Facts.FromTo arg) = |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26268
diff
changeset
|
271 |
"Facts.FromTo " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int arg |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26268
diff
changeset
|
272 |
| print_interval (Facts.From i) = "Facts.From " ^ ML_Syntax.print_int i |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26268
diff
changeset
|
273 |
| print_interval (Facts.Single i) = "Facts.Single " ^ ML_Syntax.print_int i; |
24574 | 274 |
|
26368
3e74b09ce466
thm_antiq: produce error at runtime, not compile time;
wenzelm
parents:
26361
diff
changeset
|
275 |
fun thm_antiq kind get get_name = value_antiq kind |
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
276 |
(context -- Scan.lift (Args.position Args.name -- Scan.option Args.thm_sel) |
26374 | 277 |
>> (fn (ctxt, ((name, pos), sel)) => |
26368
3e74b09ce466
thm_antiq: produce error at runtime, not compile time;
wenzelm
parents:
26361
diff
changeset
|
278 |
let |
26374 | 279 |
val _ = get ctxt (Facts.Named ((name, pos), sel)); |
280 |
val txt = |
|
281 |
"(Facts.Named ((" ^ ML_Syntax.print_string name ^ ", Position.none), " ^ |
|
282 |
ML_Syntax.print_option (ML_Syntax.print_list print_interval) sel ^ "))"; |
|
283 |
in (name, get_name ^ " (ML_Context.the_local_context ()) " ^ txt) end)); |
|
24574 | 284 |
|
285 |
in |
|
286 |
||
287 |
val _ = add_keywords ["(", ")", "-", ","]; |
|
26368
3e74b09ce466
thm_antiq: produce error at runtime, not compile time;
wenzelm
parents:
26361
diff
changeset
|
288 |
val _ = thm_antiq "thm" ProofContext.get_fact_single "ProofContext.get_fact_single"; |
3e74b09ce466
thm_antiq: produce error at runtime, not compile time;
wenzelm
parents:
26361
diff
changeset
|
289 |
val _ = thm_antiq "thms" ProofContext.get_fact "ProofContext.get_fact"; |
24574 | 290 |
|
291 |
end; |
|
292 |
||
24685 | 293 |
val _ = proj_value_antiq "cpat" (Scan.lift Args.name >> |
294 |
(fn name => ("cpat", |
|
26432
095e448b95a0
renamed ML_Context.the_context to ML_Context.the_global_context;
wenzelm
parents:
26416
diff
changeset
|
295 |
"Thm.cterm_of (ML_Context.the_global_context ()) (Syntax.read_term \ |
24685 | 296 |
\(ProofContext.set_mode ProofContext.mode_pattern (ML_Context.the_local_context ()))" |
297 |
^ ML_Syntax.print_string name ^ ")", ""))); |
|
24574 | 298 |
|
299 |
end; |
|
300 |
||
301 |
structure Basic_ML_Context: BASIC_ML_CONTEXT = ML_Context; |
|
302 |
open Basic_ML_Context; |