author | wenzelm |
Tue, 18 Mar 2014 11:27:09 +0100 | |
changeset 56201 | dd2df97b379b |
parent 56199 | 8e8d28ed7529 |
child 56203 | 76c72f4d0667 |
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 ML_CONTEXT = |
|
8 |
sig |
|
9 |
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
|
10 |
val the_global_context: unit -> theory |
24574 | 11 |
val the_local_context: unit -> Proof.context |
39164
e7e12555e763
ML_Context.thm and ML_Context.thms no longer pervasive;
wenzelm
parents:
39140
diff
changeset
|
12 |
val thm: xstring -> thm |
e7e12555e763
ML_Context.thm and ML_Context.thms no longer pervasive;
wenzelm
parents:
39140
diff
changeset
|
13 |
val thms: xstring -> thm list |
26455 | 14 |
val exec: (unit -> unit) -> Context.generic -> Context.generic |
56070 | 15 |
val check_antiquotation: Proof.context -> xstring * Position.T -> string |
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
16 |
val print_antiquotations: Proof.context -> unit |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
17 |
type decl = Proof.context -> string * string |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
18 |
val antiquotation: binding -> 'a context_parser -> |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
19 |
(Args.src -> 'a -> Proof.context -> decl * Proof.context) -> theory -> theory |
41375 | 20 |
val trace_raw: Config.raw |
21 |
val trace: bool Config.T |
|
30637
3e3c2cd88cf1
export eval_antiquotes: refined version that operates on ML tokens;
wenzelm
parents:
30614
diff
changeset
|
22 |
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
|
23 |
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
|
24 |
val eval: bool -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55743
diff
changeset
|
25 |
val eval_source: bool -> Symbol_Pos.source -> 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
|
26 |
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
|
27 |
ML_Lex.token Antiquote.antiquote list -> unit |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55743
diff
changeset
|
28 |
val eval_source_in: Proof.context option -> bool -> Symbol_Pos.source -> 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
|
29 |
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
|
30 |
Context.generic -> Context.generic |
25204 | 31 |
end |
24574 | 32 |
|
33 |
structure ML_Context: ML_CONTEXT = |
|
34 |
struct |
|
35 |
||
26416
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
36 |
(** implicit ML context **) |
24574 | 37 |
|
26416
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
38 |
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
|
39 |
val the_global_context = Context.theory_of o the_generic_context; |
24574 | 40 |
val the_local_context = Context.proof_of o the_generic_context; |
41 |
||
42360 | 42 |
fun thm name = Proof_Context.get_thm (the_local_context ()) name; |
43 |
fun thms name = Proof_Context.get_thms (the_local_context ()) name; |
|
39164
e7e12555e763
ML_Context.thm and ML_Context.thms no longer pervasive;
wenzelm
parents:
39140
diff
changeset
|
44 |
|
26455 | 45 |
fun exec (e: unit -> unit) context = |
46 |
(case Context.setmp_thread_data (SOME context) (fn () => (e (); Context.thread_data ())) () of |
|
47 |
SOME context' => context' |
|
48 |
| NONE => error "Missing context after execution"); |
|
26416
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
49 |
|
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
50 |
|
24574 | 51 |
|
52 |
(** ML antiquotations **) |
|
53 |
||
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
54 |
(* theory data *) |
27343
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
55 |
|
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
56 |
type decl = Proof.context -> string * string; (*final context -> ML env, ML body*) |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
57 |
structure Antiquotations = Theory_Data |
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
58 |
( |
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
59 |
type T = (Args.src -> Proof.context -> decl * Proof.context) Name_Space.table; |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
48992
diff
changeset
|
60 |
val empty : T = Name_Space.empty_table Markup.ML_antiquotationN; |
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
61 |
val extend = I; |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
62 |
fun merge data : T = Name_Space.merge_tables data; |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
63 |
); |
27343
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
64 |
|
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
65 |
val get_antiquotations = Antiquotations.get o Proof_Context.theory_of; |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
66 |
|
56070 | 67 |
fun check_antiquotation ctxt = |
68 |
#1 o Name_Space.check (Context.Proof ctxt) (get_antiquotations ctxt); |
|
69 |
||
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
70 |
fun add_antiquotation name f thy = thy |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
71 |
|> Antiquotations.map (Name_Space.define (Context.Theory thy) true (name, f) #> snd); |
55743 | 72 |
|
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
73 |
fun print_antiquotations ctxt = |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
74 |
Pretty.big_list "ML antiquotations:" |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
75 |
(map (Pretty.mark_str o #1) (Name_Space.markup_table ctxt (get_antiquotations ctxt))) |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
76 |
|> Pretty.writeln; |
27343
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
77 |
|
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
78 |
fun apply_antiquotation src ctxt = |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
79 |
let val (src', f) = Args.check_src ctxt (get_antiquotations ctxt) src |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
80 |
in f src' ctxt end; |
43563 | 81 |
|
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
82 |
fun antiquotation name scan body = |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
83 |
add_antiquotation name |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
84 |
(fn src => fn orig_ctxt => |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
85 |
let val (x, _) = Args.syntax scan src orig_ctxt |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
86 |
in body src x orig_ctxt end); |
27343
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
87 |
|
24574 | 88 |
|
27343
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
89 |
(* parsing and evaluation *) |
24574 | 90 |
|
27343
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
91 |
local |
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
92 |
|
24574 | 93 |
val antiq = |
56201 | 94 |
Parse.!!! (Parse.position Parse.xname -- Parse.args --| Scan.ahead Parse.eof) |
56029
8bedca4bd5a3
clarified Args.src: more abstract type, position refers to name only;
wenzelm
parents:
55828
diff
changeset
|
95 |
>> uncurry Args.src; |
24574 | 96 |
|
48776
37cd53e69840
faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
wenzelm
parents:
47005
diff
changeset
|
97 |
val begin_env0 = ML_Lex.tokenize "structure Isabelle =\nstruct\n"; |
52663
6e71d43775e5
retain compile-time context visibility, which is particularly important for "apply tactic";
wenzelm
parents:
50201
diff
changeset
|
98 |
|
6e71d43775e5
retain compile-time context visibility, which is particularly important for "apply tactic";
wenzelm
parents:
50201
diff
changeset
|
99 |
fun begin_env visible = |
48776
37cd53e69840
faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
wenzelm
parents:
47005
diff
changeset
|
100 |
ML_Lex.tokenize |
52663
6e71d43775e5
retain compile-time context visibility, which is particularly important for "apply tactic";
wenzelm
parents:
50201
diff
changeset
|
101 |
("structure Isabelle =\nstruct\n\ |
6e71d43775e5
retain compile-time context visibility, which is particularly important for "apply tactic";
wenzelm
parents:
50201
diff
changeset
|
102 |
\val ML_context = Context_Position.set_visible " ^ Bool.toString visible ^ |
6e71d43775e5
retain compile-time context visibility, which is particularly important for "apply tactic";
wenzelm
parents:
50201
diff
changeset
|
103 |
" (ML_Context.the_local_context ());\n"); |
48776
37cd53e69840
faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
wenzelm
parents:
47005
diff
changeset
|
104 |
|
30637
3e3c2cd88cf1
export eval_antiquotes: refined version that operates on ML tokens;
wenzelm
parents:
30614
diff
changeset
|
105 |
val end_env = ML_Lex.tokenize "end;"; |
31334 | 106 |
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
|
107 |
|
30637
3e3c2cd88cf1
export eval_antiquotes: refined version that operates on ML tokens;
wenzelm
parents:
30614
diff
changeset
|
108 |
in |
3e3c2cd88cf1
export eval_antiquotes: refined version that operates on ML tokens;
wenzelm
parents:
30614
diff
changeset
|
109 |
|
3e3c2cd88cf1
export eval_antiquotes: refined version that operates on ML tokens;
wenzelm
parents:
30614
diff
changeset
|
110 |
fun eval_antiquotes (ants, pos) opt_context = |
24574 | 111 |
let |
52663
6e71d43775e5
retain compile-time context visibility, which is particularly important for "apply tactic";
wenzelm
parents:
50201
diff
changeset
|
112 |
val visible = |
6e71d43775e5
retain compile-time context visibility, which is particularly important for "apply tactic";
wenzelm
parents:
50201
diff
changeset
|
113 |
(case opt_context of |
6e71d43775e5
retain compile-time context visibility, which is particularly important for "apply tactic";
wenzelm
parents:
50201
diff
changeset
|
114 |
SOME (Context.Proof ctxt) => Context_Position.is_visible ctxt |
6e71d43775e5
retain compile-time context visibility, which is particularly important for "apply tactic";
wenzelm
parents:
50201
diff
changeset
|
115 |
| _ => true); |
28270
7ada24ebea94
explicit handling of ML environment within generic context;
wenzelm
parents:
27895
diff
changeset
|
116 |
val opt_ctxt = Option.map (Context.Proof o Context.proof_of) opt_context; |
52663
6e71d43775e5
retain compile-time context visibility, which is particularly important for "apply tactic";
wenzelm
parents:
50201
diff
changeset
|
117 |
|
27343
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
118 |
val ((ml_env, ml_body), opt_ctxt') = |
30637
3e3c2cd88cf1
export eval_antiquotes: refined version that operates on ML tokens;
wenzelm
parents:
30614
diff
changeset
|
119 |
if forall Antiquote.is_text ants |
48776
37cd53e69840
faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
wenzelm
parents:
47005
diff
changeset
|
120 |
then ((begin_env0, map (fn Antiquote.Text tok => tok) ants), opt_ctxt) |
27343
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
121 |
else |
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
122 |
let |
53167 | 123 |
val lex = #1 (Keyword.get_lexicons ()); |
124 |
fun no_decl _ = ([], []); |
|
125 |
||
126 |
fun expand (Antiquote.Text tok) ctxt = (K ([], [tok]), ctxt) |
|
55526 | 127 |
| expand (Antiquote.Antiq (ss, {range, ...})) ctxt = |
53167 | 128 |
let |
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
129 |
val (decl, ctxt') = |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
130 |
apply_antiquotation (Token.read_antiq lex antiq (ss, #1 range)) ctxt; |
53167 | 131 |
val decl' = decl #> pairself (ML_Lex.tokenize #> map (ML_Lex.set_range range)); |
132 |
in (decl', ctxt') end; |
|
133 |
||
27343
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
134 |
val ctxt = |
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
135 |
(case opt_ctxt of |
48992 | 136 |
NONE => error ("No context -- cannot expand ML antiquotations" ^ Position.here pos) |
28270
7ada24ebea94
explicit handling of ML environment within generic context;
wenzelm
parents:
27895
diff
changeset
|
137 |
| SOME ctxt => Context.proof_of ctxt); |
27378 | 138 |
|
53167 | 139 |
val (decls, ctxt') = fold_map expand ants ctxt; |
52663
6e71d43775e5
retain compile-time context visibility, which is particularly important for "apply tactic";
wenzelm
parents:
50201
diff
changeset
|
140 |
val (ml_env, ml_body) = |
6e71d43775e5
retain compile-time context visibility, which is particularly important for "apply tactic";
wenzelm
parents:
50201
diff
changeset
|
141 |
decls |> map (fn decl => decl ctxt') |> split_list |> pairself flat; |
6e71d43775e5
retain compile-time context visibility, which is particularly important for "apply tactic";
wenzelm
parents:
50201
diff
changeset
|
142 |
in ((begin_env visible @ ml_env, ml_body), SOME (Context.Proof ctxt')) end; |
48776
37cd53e69840
faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
wenzelm
parents:
47005
diff
changeset
|
143 |
in ((ml_env @ end_env, ml_body), opt_ctxt') end; |
24574 | 144 |
|
41375 | 145 |
val trace_raw = Config.declare "ML_trace" (fn _ => Config.Bool false); |
146 |
val trace = Config.bool trace_raw; |
|
24574 | 147 |
|
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
|
148 |
fun eval verbose pos ants = |
24574 | 149 |
let |
28270
7ada24ebea94
explicit handling of ML environment within generic context;
wenzelm
parents:
27895
diff
changeset
|
150 |
(*prepare source text*) |
41485
6c0de045d127
ML_trace: observe context visibility flag (import for Latex mode, for example);
wenzelm
parents:
41375
diff
changeset
|
151 |
val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ()); |
31334 | 152 |
val _ = |
41485
6c0de045d127
ML_trace: observe context visibility flag (import for Latex mode, for example);
wenzelm
parents:
41375
diff
changeset
|
153 |
(case Option.map Context.proof_of env_ctxt of |
6c0de045d127
ML_trace: observe context visibility flag (import for Latex mode, for example);
wenzelm
parents:
41375
diff
changeset
|
154 |
SOME ctxt => |
6c0de045d127
ML_trace: observe context visibility flag (import for Latex mode, for example);
wenzelm
parents:
41375
diff
changeset
|
155 |
if Config.get ctxt trace then |
6c0de045d127
ML_trace: observe context visibility flag (import for Latex mode, for example);
wenzelm
parents:
41375
diff
changeset
|
156 |
Context_Position.if_visible ctxt |
6c0de045d127
ML_trace: observe context visibility flag (import for Latex mode, for example);
wenzelm
parents:
41375
diff
changeset
|
157 |
tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body]) |
41375 | 158 |
else () |
159 |
| NONE => ()); |
|
28270
7ada24ebea94
explicit handling of ML environment within generic context;
wenzelm
parents:
27895
diff
changeset
|
160 |
|
7ada24ebea94
explicit handling of ML environment within generic context;
wenzelm
parents:
27895
diff
changeset
|
161 |
(*prepare static ML environment*) |
41485
6c0de045d127
ML_trace: observe context visibility flag (import for Latex mode, for example);
wenzelm
parents:
41375
diff
changeset
|
162 |
val _ = |
6c0de045d127
ML_trace: observe context visibility flag (import for Latex mode, for example);
wenzelm
parents:
41375
diff
changeset
|
163 |
Context.setmp_thread_data |
6c0de045d127
ML_trace: observe context visibility flag (import for Latex mode, for example);
wenzelm
parents:
41375
diff
changeset
|
164 |
(Option.map (Context.mapping I (Context_Position.set_visible false)) env_ctxt) |
31334 | 165 |
(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
|
166 |
|> (fn NONE => () | SOME context' => Context.>> (ML_Env.inherit context')); |
28270
7ada24ebea94
explicit handling of ML environment within generic context;
wenzelm
parents:
27895
diff
changeset
|
167 |
|
31334 | 168 |
val _ = ML_Compiler.eval verbose pos body; |
169 |
val _ = ML_Compiler.eval false Position.none reset_env; |
|
28270
7ada24ebea94
explicit handling of ML environment within generic context;
wenzelm
parents:
27895
diff
changeset
|
170 |
in () end; |
24574 | 171 |
|
172 |
end; |
|
173 |
||
174 |
||
30672
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents:
30643
diff
changeset
|
175 |
(* derived versions *) |
24574 | 176 |
|
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55743
diff
changeset
|
177 |
fun eval_source verbose source = |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55743
diff
changeset
|
178 |
eval verbose (#pos source) (ML_Lex.read_source source); |
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
|
179 |
|
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_in ctxt verbose pos ants = |
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
181 |
Context.setmp_thread_data (Option.map Context.Proof ctxt) |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
182 |
(fn () => eval verbose pos ants) (); |
24574 | 183 |
|
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55743
diff
changeset
|
184 |
fun eval_source_in ctxt verbose source = |
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
185 |
Context.setmp_thread_data (Option.map Context.Proof ctxt) |
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
186 |
(fn () => eval_source verbose source) (); |
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
|
187 |
|
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
|
188 |
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
|
189 |
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
|
190 |
(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
|
191 |
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
|
192 |
|
24574 | 193 |
end; |
194 |