author | wenzelm |
Fri, 17 Sep 2010 20:18:27 +0200 | |
changeset 39507 | 839873937ddd |
parent 39388 | fdbb2c55ffc2 |
child 39557 | fe5722fce758 |
permissions | -rw-r--r-- |
24581 | 1 |
(* Title: Pure/ML/ml_context.ML |
24574 | 2 |
Author: Makarius |
3 |
||
4 |
ML context and antiquotations. |
|
5 |
*) |
|
6 |
||
7 |
signature BASIC_ML_CONTEXT = |
|
8 |
sig |
|
26416
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
9 |
val bind_thm: string * thm -> unit |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
10 |
val bind_thms: string * thm list -> unit |
25204 | 11 |
end |
24574 | 12 |
|
13 |
signature ML_CONTEXT = |
|
14 |
sig |
|
15 |
include BASIC_ML_CONTEXT |
|
16 |
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
|
17 |
val the_global_context: unit -> theory |
24574 | 18 |
val the_local_context: unit -> Proof.context |
39164
e7e12555e763
ML_Context.thm and ML_Context.thms no longer pervasive;
wenzelm
parents:
39140
diff
changeset
|
19 |
val thm: xstring -> thm |
e7e12555e763
ML_Context.thm and ML_Context.thms no longer pervasive;
wenzelm
parents:
39140
diff
changeset
|
20 |
val thms: xstring -> thm list |
26455 | 21 |
val exec: (unit -> unit) -> Context.generic -> Context.generic |
39140
8a2fb4ce1f39
ML_Context.ml_store_thm(s): operate on thread context instead of Unsynchronized.ref;
wenzelm
parents:
38931
diff
changeset
|
22 |
val get_stored_thms: unit -> thm list |
8a2fb4ce1f39
ML_Context.ml_store_thm(s): operate on thread context instead of Unsynchronized.ref;
wenzelm
parents:
38931
diff
changeset
|
23 |
val get_stored_thm: unit -> thm |
8a2fb4ce1f39
ML_Context.ml_store_thm(s): operate on thread context instead of Unsynchronized.ref;
wenzelm
parents:
38931
diff
changeset
|
24 |
val ml_store_thms: string * thm list -> unit |
26416
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
25 |
val ml_store_thm: string * thm -> unit |
35019
1ec0a3ff229e
simplified interface for ML antiquotations, struct_name is always "Isabelle";
wenzelm
parents:
33222
diff
changeset
|
26 |
type antiq = Proof.context -> (Proof.context -> string * string) * Proof.context |
30513 | 27 |
val add_antiq: string -> (Position.T -> antiq context_parser) -> unit |
32738 | 28 |
val trace: bool Unsynchronized.ref |
30637
3e3c2cd88cf1
export eval_antiquotes: refined version that operates on ML tokens;
wenzelm
parents:
30614
diff
changeset
|
29 |
val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T -> |
3e3c2cd88cf1
export eval_antiquotes: refined version that operates on ML tokens;
wenzelm
parents:
30614
diff
changeset
|
30 |
Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option |
37198
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
36959
diff
changeset
|
31 |
val eval: bool -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit |
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
36959
diff
changeset
|
32 |
val eval_text: bool -> Position.T -> Symbol_Pos.text -> unit |
26455 | 33 |
val eval_file: Path.T -> unit |
37198
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
36959
diff
changeset
|
34 |
val eval_in: Proof.context option -> bool -> Position.T -> |
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
36959
diff
changeset
|
35 |
ML_Lex.token Antiquote.antiquote list -> unit |
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
36959
diff
changeset
|
36 |
val eval_text_in: Proof.context option -> bool -> Position.T -> Symbol_Pos.text -> unit |
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
36959
diff
changeset
|
37 |
val expression: Position.T -> string -> string -> ML_Lex.token Antiquote.antiquote list -> |
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
36959
diff
changeset
|
38 |
Context.generic -> Context.generic |
39388
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
haftmann
parents:
39164
diff
changeset
|
39 |
val value: Proof.context -> |
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
haftmann
parents:
39164
diff
changeset
|
40 |
(Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string -> |
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
haftmann
parents:
39164
diff
changeset
|
41 |
string * string -> 'a |
25204 | 42 |
end |
24574 | 43 |
|
44 |
structure ML_Context: ML_CONTEXT = |
|
45 |
struct |
|
46 |
||
26416
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
47 |
(** implicit ML context **) |
24574 | 48 |
|
26416
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
49 |
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
|
50 |
val the_global_context = Context.theory_of o the_generic_context; |
24574 | 51 |
val the_local_context = Context.proof_of o the_generic_context; |
52 |
||
39164
e7e12555e763
ML_Context.thm and ML_Context.thms no longer pervasive;
wenzelm
parents:
39140
diff
changeset
|
53 |
fun thm name = ProofContext.get_thm (the_local_context ()) name; |
e7e12555e763
ML_Context.thm and ML_Context.thms no longer pervasive;
wenzelm
parents:
39140
diff
changeset
|
54 |
fun thms name = ProofContext.get_thms (the_local_context ()) name; |
e7e12555e763
ML_Context.thm and ML_Context.thms no longer pervasive;
wenzelm
parents:
39140
diff
changeset
|
55 |
|
26455 | 56 |
fun exec (e: unit -> unit) context = |
57 |
(case Context.setmp_thread_data (SOME context) (fn () => (e (); Context.thread_data ())) () of |
|
58 |
SOME context' => context' |
|
59 |
| NONE => error "Missing context after execution"); |
|
26416
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
60 |
|
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
61 |
|
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
62 |
(* theorem bindings *) |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
63 |
|
39140
8a2fb4ce1f39
ML_Context.ml_store_thm(s): operate on thread context instead of Unsynchronized.ref;
wenzelm
parents:
38931
diff
changeset
|
64 |
structure Stored_Thms = Theory_Data |
8a2fb4ce1f39
ML_Context.ml_store_thm(s): operate on thread context instead of Unsynchronized.ref;
wenzelm
parents:
38931
diff
changeset
|
65 |
( |
8a2fb4ce1f39
ML_Context.ml_store_thm(s): operate on thread context instead of Unsynchronized.ref;
wenzelm
parents:
38931
diff
changeset
|
66 |
type T = thm list; |
8a2fb4ce1f39
ML_Context.ml_store_thm(s): operate on thread context instead of Unsynchronized.ref;
wenzelm
parents:
38931
diff
changeset
|
67 |
val empty = []; |
8a2fb4ce1f39
ML_Context.ml_store_thm(s): operate on thread context instead of Unsynchronized.ref;
wenzelm
parents:
38931
diff
changeset
|
68 |
fun extend _ = []; |
8a2fb4ce1f39
ML_Context.ml_store_thm(s): operate on thread context instead of Unsynchronized.ref;
wenzelm
parents:
38931
diff
changeset
|
69 |
fun merge _ = []; |
8a2fb4ce1f39
ML_Context.ml_store_thm(s): operate on thread context instead of Unsynchronized.ref;
wenzelm
parents:
38931
diff
changeset
|
70 |
); |
26416
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
71 |
|
39140
8a2fb4ce1f39
ML_Context.ml_store_thm(s): operate on thread context instead of Unsynchronized.ref;
wenzelm
parents:
38931
diff
changeset
|
72 |
fun get_stored_thms () = Stored_Thms.get (the_global_context ()); |
8a2fb4ce1f39
ML_Context.ml_store_thm(s): operate on thread context instead of Unsynchronized.ref;
wenzelm
parents:
38931
diff
changeset
|
73 |
val get_stored_thm = hd o get_stored_thms; |
8a2fb4ce1f39
ML_Context.ml_store_thm(s): operate on thread context instead of Unsynchronized.ref;
wenzelm
parents:
38931
diff
changeset
|
74 |
|
8a2fb4ce1f39
ML_Context.ml_store_thm(s): operate on thread context instead of Unsynchronized.ref;
wenzelm
parents:
38931
diff
changeset
|
75 |
fun ml_store get (name, ths) = |
26492
6e87cc839632
removed obsolete store_thm(s), cf. functional versions in pure_thy.ML;
wenzelm
parents:
26473
diff
changeset
|
76 |
let |
29579 | 77 |
val ths' = Context.>>> (Context.map_theory_result |
78 |
(PureThy.store_thms (Binding.name name, ths))); |
|
39140
8a2fb4ce1f39
ML_Context.ml_store_thm(s): operate on thread context instead of Unsynchronized.ref;
wenzelm
parents:
38931
diff
changeset
|
79 |
val _ = Context.>> (Context.map_theory (Stored_Thms.put ths')); |
26492
6e87cc839632
removed obsolete store_thm(s), cf. functional versions in pure_thy.ML;
wenzelm
parents:
26473
diff
changeset
|
80 |
val _ = |
6e87cc839632
removed obsolete store_thm(s), cf. functional versions in pure_thy.ML;
wenzelm
parents:
26473
diff
changeset
|
81 |
if name = "" then () |
6e87cc839632
removed obsolete store_thm(s), cf. functional versions in pure_thy.ML;
wenzelm
parents:
26473
diff
changeset
|
82 |
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
|
83 |
error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value") |
39140
8a2fb4ce1f39
ML_Context.ml_store_thm(s): operate on thread context instead of Unsynchronized.ref;
wenzelm
parents:
38931
diff
changeset
|
84 |
else |
31334 | 85 |
ML_Compiler.eval true Position.none |
39140
8a2fb4ce1f39
ML_Context.ml_store_thm(s): operate on thread context instead of Unsynchronized.ref;
wenzelm
parents:
38931
diff
changeset
|
86 |
(ML_Lex.tokenize ("val " ^ name ^ " = " ^ get ^ " ();")); |
8a2fb4ce1f39
ML_Context.ml_store_thm(s): operate on thread context instead of Unsynchronized.ref;
wenzelm
parents:
38931
diff
changeset
|
87 |
val _ = Context.>> (Context.map_theory (Stored_Thms.put [])); |
26492
6e87cc839632
removed obsolete store_thm(s), cf. functional versions in pure_thy.ML;
wenzelm
parents:
26473
diff
changeset
|
88 |
in () end; |
24574 | 89 |
|
39140
8a2fb4ce1f39
ML_Context.ml_store_thm(s): operate on thread context instead of Unsynchronized.ref;
wenzelm
parents:
38931
diff
changeset
|
90 |
val ml_store_thms = ml_store "ML_Context.get_stored_thms"; |
8a2fb4ce1f39
ML_Context.ml_store_thm(s): operate on thread context instead of Unsynchronized.ref;
wenzelm
parents:
38931
diff
changeset
|
91 |
fun ml_store_thm (name, th) = ml_store "ML_Context.get_stored_thm" (name, [th]); |
26416
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
92 |
|
35021
c839a4c670c6
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
35019
diff
changeset
|
93 |
fun bind_thm (name, thm) = ml_store_thm (name, Drule.export_without_context thm); |
c839a4c670c6
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
35019
diff
changeset
|
94 |
fun bind_thms (name, thms) = ml_store_thms (name, map Drule.export_without_context thms); |
24574 | 95 |
|
96 |
||
97 |
||
98 |
(** ML antiquotations **) |
|
99 |
||
27343
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
100 |
(* antiquotation commands *) |
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
101 |
|
35019
1ec0a3ff229e
simplified interface for ML antiquotations, struct_name is always "Isabelle";
wenzelm
parents:
33222
diff
changeset
|
102 |
type antiq = Proof.context -> (Proof.context -> string * string) * Proof.context; |
27343
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
103 |
|
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
104 |
local |
24574 | 105 |
|
32738 | 106 |
val global_parsers = |
107 |
Unsynchronized.ref (Symtab.empty: (Position.T -> antiq context_parser) Symtab.table); |
|
27343
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
108 |
|
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
109 |
in |
24574 | 110 |
|
27343
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
111 |
fun add_antiq name scan = CRITICAL (fn () => |
32738 | 112 |
Unsynchronized.change global_parsers (fn tab => |
27343
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
113 |
(if not (Symtab.defined tab name) then () |
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
114 |
else warning ("Redefined ML antiquotation: " ^ quote name); |
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
115 |
Symtab.update (name, scan) tab))); |
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
116 |
|
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
117 |
fun antiquotation src ctxt = |
24574 | 118 |
let val ((name, _), pos) = Args.dest_src src in |
119 |
(case Symtab.lookup (! global_parsers) name of |
|
120 |
NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos) |
|
39507
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39388
diff
changeset
|
121 |
| SOME scan => |
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39388
diff
changeset
|
122 |
(Context_Position.report ctxt pos (Markup.ML_antiq name); |
27895 | 123 |
Args.context_syntax "ML antiquotation" (scan pos) src ctxt)) |
24574 | 124 |
end; |
125 |
||
27343
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
126 |
end; |
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
127 |
|
24574 | 128 |
|
27343
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
129 |
(* parsing and evaluation *) |
24574 | 130 |
|
27343
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
131 |
local |
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
132 |
|
24574 | 133 |
val antiq = |
36950 | 134 |
Parse.!!! (Parse.position Parse.xname -- Args.parse --| Scan.ahead Parse.eof) |
24574 | 135 |
>> (fn ((x, pos), y) => Args.src ((x, y), pos)); |
136 |
||
35019
1ec0a3ff229e
simplified interface for ML antiquotations, struct_name is always "Isabelle";
wenzelm
parents:
33222
diff
changeset
|
137 |
val begin_env = ML_Lex.tokenize "structure Isabelle =\nstruct\n"; |
30637
3e3c2cd88cf1
export eval_antiquotes: refined version that operates on ML tokens;
wenzelm
parents:
30614
diff
changeset
|
138 |
val end_env = ML_Lex.tokenize "end;"; |
31334 | 139 |
val reset_env = ML_Lex.tokenize "structure Isabelle = struct end"; |
28270
7ada24ebea94
explicit handling of ML environment within generic context;
wenzelm
parents:
27895
diff
changeset
|
140 |
|
30637
3e3c2cd88cf1
export eval_antiquotes: refined version that operates on ML tokens;
wenzelm
parents:
30614
diff
changeset
|
141 |
in |
3e3c2cd88cf1
export eval_antiquotes: refined version that operates on ML tokens;
wenzelm
parents:
30614
diff
changeset
|
142 |
|
3e3c2cd88cf1
export eval_antiquotes: refined version that operates on ML tokens;
wenzelm
parents:
30614
diff
changeset
|
143 |
fun eval_antiquotes (ants, pos) opt_context = |
24574 | 144 |
let |
28270
7ada24ebea94
explicit handling of ML environment within generic context;
wenzelm
parents:
27895
diff
changeset
|
145 |
val opt_ctxt = Option.map (Context.Proof o Context.proof_of) opt_context; |
27343
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
146 |
val ((ml_env, ml_body), opt_ctxt') = |
30637
3e3c2cd88cf1
export eval_antiquotes: refined version that operates on ML tokens;
wenzelm
parents:
30614
diff
changeset
|
147 |
if forall Antiquote.is_text ants |
3e3c2cd88cf1
export eval_antiquotes: refined version that operates on ML tokens;
wenzelm
parents:
30614
diff
changeset
|
148 |
then (([], map (fn Antiquote.Text tok => tok) ants), opt_ctxt) |
27343
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
149 |
else |
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
150 |
let |
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
151 |
val ctxt = |
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
152 |
(case opt_ctxt of |
30637
3e3c2cd88cf1
export eval_antiquotes: refined version that operates on ML tokens;
wenzelm
parents:
30614
diff
changeset
|
153 |
NONE => error ("No context -- cannot expand ML antiquotations" ^ Position.str_of pos) |
28270
7ada24ebea94
explicit handling of ML environment within generic context;
wenzelm
parents:
27895
diff
changeset
|
154 |
| SOME ctxt => Context.proof_of ctxt); |
27378 | 155 |
|
36950 | 156 |
val lex = #1 (Keyword.get_lexicons ()); |
30637
3e3c2cd88cf1
export eval_antiquotes: refined version that operates on ML tokens;
wenzelm
parents:
30614
diff
changeset
|
157 |
fun no_decl _ = ([], []); |
27378 | 158 |
|
30637
3e3c2cd88cf1
export eval_antiquotes: refined version that operates on ML tokens;
wenzelm
parents:
30614
diff
changeset
|
159 |
fun expand (Antiquote.Text tok) state = (K ([], [tok]), state) |
30683
e8ac1f9d9469
datatype antiquote: maintain original Position.range, which is eventually attached to the resulting ML tokens;
wenzelm
parents:
30672
diff
changeset
|
160 |
| expand (Antiquote.Antiq (ss, range)) (scope, background) = |
27343
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
161 |
let |
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
162 |
val context = Stack.top scope; |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36950
diff
changeset
|
163 |
val (f, context') = |
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36950
diff
changeset
|
164 |
antiquotation (Token.read_antiq lex antiq (ss, #1 range)) context; |
35019
1ec0a3ff229e
simplified interface for ML antiquotations, struct_name is always "Isabelle";
wenzelm
parents:
33222
diff
changeset
|
165 |
val (decl, background') = f background; |
30683
e8ac1f9d9469
datatype antiquote: maintain original Position.range, which is eventually attached to the resulting ML tokens;
wenzelm
parents:
30672
diff
changeset
|
166 |
val decl' = decl #> pairself (ML_Lex.tokenize #> map (ML_Lex.set_range range)); |
30637
3e3c2cd88cf1
export eval_antiquotes: refined version that operates on ML tokens;
wenzelm
parents:
30614
diff
changeset
|
167 |
in (decl', (Stack.map_top (K context') scope, background')) end |
27343
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
168 |
| expand (Antiquote.Open _) (scope, background) = |
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
169 |
(no_decl, (Stack.push scope, background)) |
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
170 |
| expand (Antiquote.Close _) (scope, background) = |
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
171 |
(no_decl, (Stack.pop scope, background)); |
24574 | 172 |
|
27343
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
173 |
val (decls, (_, ctxt')) = fold_map expand ants (Stack.init ctxt, ctxt); |
30637
3e3c2cd88cf1
export eval_antiquotes: refined version that operates on ML tokens;
wenzelm
parents:
30614
diff
changeset
|
174 |
val ml = decls |> map (fn decl => decl ctxt') |> split_list |> pairself flat; |
27343
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
175 |
in (ml, SOME (Context.Proof ctxt')) end; |
30637
3e3c2cd88cf1
export eval_antiquotes: refined version that operates on ML tokens;
wenzelm
parents:
30614
diff
changeset
|
176 |
in ((begin_env @ ml_env @ end_env, ml_body), opt_ctxt') end; |
24574 | 177 |
|
32738 | 178 |
val trace = Unsynchronized.ref false; |
24574 | 179 |
|
37198
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
36959
diff
changeset
|
180 |
fun eval verbose pos ants = |
24574 | 181 |
let |
28270
7ada24ebea94
explicit handling of ML environment within generic context;
wenzelm
parents:
27895
diff
changeset
|
182 |
(*prepare source text*) |
38720
7f8bc335e203
ML_Context.eval: produce antiquotation environment preferably in invisible context, to avoid displaced report messages from ML_Compiler;
wenzelm
parents:
38237
diff
changeset
|
183 |
val ((env, body), env_ctxt) = |
7f8bc335e203
ML_Context.eval: produce antiquotation environment preferably in invisible context, to avoid displaced report messages from ML_Compiler;
wenzelm
parents:
38237
diff
changeset
|
184 |
eval_antiquotes (ants, pos) (Context.thread_data ()) |
7f8bc335e203
ML_Context.eval: produce antiquotation environment preferably in invisible context, to avoid displaced report messages from ML_Compiler;
wenzelm
parents:
38237
diff
changeset
|
185 |
||> Option.map (Context.mapping I (Context_Position.set_visible false)); |
31334 | 186 |
val _ = |
187 |
if ! trace then tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body]) |
|
188 |
else (); |
|
28270
7ada24ebea94
explicit handling of ML environment within generic context;
wenzelm
parents:
27895
diff
changeset
|
189 |
|
7ada24ebea94
explicit handling of ML environment within generic context;
wenzelm
parents:
27895
diff
changeset
|
190 |
(*prepare static ML environment*) |
7ada24ebea94
explicit handling of ML environment within generic context;
wenzelm
parents:
27895
diff
changeset
|
191 |
val _ = Context.setmp_thread_data env_ctxt |
31334 | 192 |
(fn () => (ML_Compiler.eval false Position.none env; Context.thread_data ())) () |
31325
700951b53d21
moved local ML environment to separate module ML_Env;
wenzelm
parents:
30683
diff
changeset
|
193 |
|> (fn NONE => () | SOME context' => Context.>> (ML_Env.inherit context')); |
28270
7ada24ebea94
explicit handling of ML environment within generic context;
wenzelm
parents:
27895
diff
changeset
|
194 |
|
31334 | 195 |
val _ = ML_Compiler.eval verbose pos body; |
196 |
val _ = ML_Compiler.eval false Position.none reset_env; |
|
28270
7ada24ebea94
explicit handling of ML environment within generic context;
wenzelm
parents:
27895
diff
changeset
|
197 |
in () end; |
24574 | 198 |
|
199 |
end; |
|
200 |
||
201 |
||
30672
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents:
30643
diff
changeset
|
202 |
(* derived versions *) |
24574 | 203 |
|
37198
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
36959
diff
changeset
|
204 |
fun eval_text verbose pos txt = eval verbose pos (ML_Lex.read pos txt); |
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
36959
diff
changeset
|
205 |
fun eval_file path = eval_text true (Path.position path) (File.read path); |
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
36959
diff
changeset
|
206 |
|
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
36959
diff
changeset
|
207 |
fun eval_in ctxt verbose pos ants = |
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
36959
diff
changeset
|
208 |
Context.setmp_thread_data (Option.map Context.Proof ctxt) (fn () => eval verbose pos ants) (); |
24574 | 209 |
|
37198
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
36959
diff
changeset
|
210 |
fun eval_text_in ctxt verbose pos txt = |
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
36959
diff
changeset
|
211 |
Context.setmp_thread_data (Option.map Context.Proof ctxt) (fn () => eval_text verbose pos txt) (); |
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
36959
diff
changeset
|
212 |
|
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
36959
diff
changeset
|
213 |
fun expression pos bind body ants = |
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
36959
diff
changeset
|
214 |
exec (fn () => eval false pos |
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
36959
diff
changeset
|
215 |
(ML_Lex.read Position.none ("Context.set_thread_data (SOME (let " ^ bind ^ " = ") @ ants @ |
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
36959
diff
changeset
|
216 |
ML_Lex.read Position.none (" in " ^ body ^ " end (ML_Context.the_generic_context ())));"))); |
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
36959
diff
changeset
|
217 |
|
39388
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
haftmann
parents:
39164
diff
changeset
|
218 |
fun value ctxt (get, put, put_ml) (prelude, value) = |
25204 | 219 |
let |
39388
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
haftmann
parents:
39164
diff
changeset
|
220 |
val read = ML_Lex.read Position.none; |
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
haftmann
parents:
39164
diff
changeset
|
221 |
val ants = read prelude @ read ("val _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml |
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
haftmann
parents:
39164
diff
changeset
|
222 |
^ " (fn () => " ^ value ^ ")) (ML_Context.the_generic_context ())))"); |
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
haftmann
parents:
39164
diff
changeset
|
223 |
val ctxt' = ctxt |
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
haftmann
parents:
39164
diff
changeset
|
224 |
|> put (fn () => error ("Bad evaluation for " ^ quote put_ml)) |
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
haftmann
parents:
39164
diff
changeset
|
225 |
|> Context.proof_map (exec (fn () => eval false Position.none ants)); |
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
haftmann
parents:
39164
diff
changeset
|
226 |
in get ctxt' () end; |
24574 | 227 |
|
228 |
end; |
|
229 |
||
230 |
structure Basic_ML_Context: BASIC_ML_CONTEXT = ML_Context; |
|
231 |
open Basic_ML_Context; |