author | wenzelm |
Tue, 05 Apr 2016 20:03:24 +0200 | |
changeset 62876 | 507c90523113 |
parent 62873 | 2f9c8a18f832 |
child 62878 | 1cec457e0a03 |
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 |
|
39164
e7e12555e763
ML_Context.thm and ML_Context.thms no longer pervasive;
wenzelm
parents:
39140
diff
changeset
|
9 |
val thm: xstring -> thm |
e7e12555e763
ML_Context.thm and ML_Context.thms no longer pervasive;
wenzelm
parents:
39140
diff
changeset
|
10 |
val thms: xstring -> thm list |
26455 | 11 |
val exec: (unit -> unit) -> Context.generic -> Context.generic |
56070 | 12 |
val check_antiquotation: Proof.context -> xstring * Position.T -> string |
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
13 |
val struct_name: Proof.context -> string |
59112 | 14 |
val variant: string -> Proof.context -> string * Proof.context |
56205 | 15 |
type decl = Proof.context -> string * string |
59112 | 16 |
val value_decl: string -> string -> Proof.context -> decl * Proof.context |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57834
diff
changeset
|
17 |
val add_antiquotation: binding -> (Token.src -> Proof.context -> decl * Proof.context) -> |
56205 | 18 |
theory -> theory |
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
59127
diff
changeset
|
19 |
val print_antiquotations: bool -> Proof.context -> unit |
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56229
diff
changeset
|
20 |
val eval: ML_Compiler.flags -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56229
diff
changeset
|
21 |
val eval_file: ML_Compiler.flags -> Path.T -> unit |
59064 | 22 |
val eval_source: ML_Compiler.flags -> Input.source -> unit |
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56229
diff
changeset
|
23 |
val eval_in: Proof.context option -> ML_Compiler.flags -> Position.T -> |
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 |
ML_Lex.token Antiquote.antiquote list -> unit |
59064 | 25 |
val eval_source_in: Proof.context option -> ML_Compiler.flags -> Input.source -> unit |
58991
92b6f4e68c5a
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
58979
diff
changeset
|
26 |
val expression: Position.range -> string -> string -> string -> |
58978
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58928
diff
changeset
|
27 |
ML_Lex.token Antiquote.antiquote list -> Context.generic -> Context.generic |
25204 | 28 |
end |
24574 | 29 |
|
30 |
structure ML_Context: ML_CONTEXT = |
|
31 |
struct |
|
32 |
||
26416
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
33 |
(** implicit ML context **) |
24574 | 34 |
|
62876 | 35 |
fun thm name = Proof_Context.get_thm (Context.the_local_context ()) name; |
36 |
fun thms name = Proof_Context.get_thms (Context.the_local_context ()) name; |
|
39164
e7e12555e763
ML_Context.thm and ML_Context.thms no longer pervasive;
wenzelm
parents:
39140
diff
changeset
|
37 |
|
26455 | 38 |
fun exec (e: unit -> unit) context = |
39 |
(case Context.setmp_thread_data (SOME context) (fn () => (e (); Context.thread_data ())) () of |
|
40 |
SOME context' => context' |
|
41 |
| NONE => error "Missing context after execution"); |
|
26416
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
42 |
|
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
43 |
|
24574 | 44 |
|
45 |
(** ML antiquotations **) |
|
46 |
||
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
47 |
(* names for generated environment *) |
59112 | 48 |
|
49 |
structure Names = Proof_Data |
|
50 |
( |
|
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
51 |
type T = string * Name.context; |
59112 | 52 |
val init_names = ML_Syntax.reserved |> fold Name.declare ["ML_context", "ML_print_depth"]; |
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
53 |
fun init _ = ("Isabelle0", init_names); |
59112 | 54 |
); |
55 |
||
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
56 |
fun struct_name ctxt = #1 (Names.get ctxt); |
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
57 |
val struct_begin = (Names.map o apfst) (fn _ => "Isabelle" ^ serial_string ()); |
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
58 |
|
59112 | 59 |
fun variant a ctxt = |
60 |
let |
|
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
61 |
val names = #2 (Names.get ctxt); |
59112 | 62 |
val (b, names') = Name.variant (Name.desymbolize (SOME false) a) names; |
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
63 |
val ctxt' = (Names.map o apsnd) (K names') ctxt; |
59112 | 64 |
in (b, ctxt') end; |
65 |
||
66 |
||
67 |
(* decl *) |
|
68 |
||
69 |
type decl = Proof.context -> string * string; (*final context -> ML env, ML body*) |
|
70 |
||
71 |
fun value_decl a s ctxt = |
|
72 |
let |
|
73 |
val (b, ctxt') = variant a ctxt; |
|
74 |
val env = "val " ^ b ^ " = " ^ s ^ ";\n"; |
|
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
75 |
val body = struct_name ctxt ^ "." ^ b; |
59112 | 76 |
fun decl (_: Proof.context) = (env, body); |
77 |
in (decl, ctxt') end; |
|
78 |
||
79 |
||
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
80 |
(* theory data *) |
27343
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
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 |
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
|
83 |
( |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57834
diff
changeset
|
84 |
type T = (Token.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
|
85 |
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
|
86 |
val extend = I; |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
87 |
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
|
88 |
); |
27343
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
89 |
|
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
90 |
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
|
91 |
|
56070 | 92 |
fun check_antiquotation ctxt = |
93 |
#1 o Name_Space.check (Context.Proof ctxt) (get_antiquotations ctxt); |
|
94 |
||
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
95 |
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
|
96 |
|> Antiquotations.map (Name_Space.define (Context.Theory thy) true (name, f) #> snd); |
55743 | 97 |
|
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
59127
diff
changeset
|
98 |
fun print_antiquotations verbose ctxt = |
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
99 |
Pretty.big_list "ML antiquotations:" |
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
59127
diff
changeset
|
100 |
(map (Pretty.mark_str o #1) (Name_Space.markup_table verbose ctxt (get_antiquotations ctxt))) |
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
101 |
|> Pretty.writeln; |
27343
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
102 |
|
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
103 |
fun apply_antiquotation src ctxt = |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61596
diff
changeset
|
104 |
let val (src', f) = Token.check_src ctxt get_antiquotations src |
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
56032
diff
changeset
|
105 |
in f src' ctxt end; |
43563 | 106 |
|
24574 | 107 |
|
27343
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
108 |
(* parsing and evaluation *) |
24574 | 109 |
|
27343
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
110 |
local |
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
111 |
|
24574 | 112 |
val antiq = |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61596
diff
changeset
|
113 |
Parse.!!! ((Parse.token Parse.xname ::: Parse.args) --| Scan.ahead Parse.eof); |
24574 | 114 |
|
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
115 |
fun make_env name visible = |
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
116 |
(ML_Lex.tokenize |
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
117 |
("structure " ^ name ^ " =\nstruct\n\ |
52663
6e71d43775e5
retain compile-time context visibility, which is particularly important for "apply tactic";
wenzelm
parents:
50201
diff
changeset
|
118 |
\val ML_context = Context_Position.set_visible " ^ Bool.toString visible ^ |
62876 | 119 |
" (Context.the_local_context ());\n\ |
57834
0d295e339f52
prefer dynamic ML_print_depth if context happens to be available;
wenzelm
parents:
57832
diff
changeset
|
120 |
\val ML_print_depth =\n\ |
0d295e339f52
prefer dynamic ML_print_depth if context happens to be available;
wenzelm
parents:
57832
diff
changeset
|
121 |
\ let val default = ML_Options.get_print_depth ()\n\ |
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
122 |
\ in fn () => ML_Options.get_print_depth_default default end;\n"), |
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
123 |
ML_Lex.tokenize "end;"); |
48776
37cd53e69840
faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
wenzelm
parents:
47005
diff
changeset
|
124 |
|
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
125 |
fun reset_env name = ML_Lex.tokenize ("structure " ^ name ^ " = struct end"); |
28270
7ada24ebea94
explicit handling of ML environment within generic context;
wenzelm
parents:
27895
diff
changeset
|
126 |
|
30637
3e3c2cd88cf1
export eval_antiquotes: refined version that operates on ML tokens;
wenzelm
parents:
30614
diff
changeset
|
127 |
fun eval_antiquotes (ants, pos) opt_context = |
24574 | 128 |
let |
52663
6e71d43775e5
retain compile-time context visibility, which is particularly important for "apply tactic";
wenzelm
parents:
50201
diff
changeset
|
129 |
val visible = |
6e71d43775e5
retain compile-time context visibility, which is particularly important for "apply tactic";
wenzelm
parents:
50201
diff
changeset
|
130 |
(case opt_context of |
6e71d43775e5
retain compile-time context visibility, which is particularly important for "apply tactic";
wenzelm
parents:
50201
diff
changeset
|
131 |
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
|
132 |
| _ => true); |
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
133 |
val opt_ctxt = Option.map Context.proof_of opt_context; |
52663
6e71d43775e5
retain compile-time context visibility, which is particularly important for "apply tactic";
wenzelm
parents:
50201
diff
changeset
|
134 |
|
27343
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
135 |
val ((ml_env, ml_body), opt_ctxt') = |
61596 | 136 |
if forall (fn Antiquote.Text _ => true | _ => false) ants |
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
137 |
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
|
138 |
else |
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
139 |
let |
59112 | 140 |
fun tokenize range = apply2 (ML_Lex.tokenize #> map (ML_Lex.set_range range)); |
53167 | 141 |
|
61471 | 142 |
fun expand_src range src ctxt = |
143 |
let val (decl, ctxt') = apply_antiquotation src ctxt |
|
144 |
in (decl #> tokenize range, ctxt') end; |
|
145 |
||
61596 | 146 |
fun expand (Antiquote.Text tok) ctxt = (K ([], [tok]), ctxt) |
61473
34d1913f0b20
clarified control antiquotations: decode control symbol to get name;
wenzelm
parents:
61471
diff
changeset
|
147 |
| expand (Antiquote.Control {name, range, body}) ctxt = |
61595 | 148 |
expand_src range |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61596
diff
changeset
|
149 |
(Token.make_src name (if null body then [] else [Token.read_cartouche body])) ctxt |
61473
34d1913f0b20
clarified control antiquotations: decode control symbol to get name;
wenzelm
parents:
61471
diff
changeset
|
150 |
| expand (Antiquote.Antiq {range, body, ...}) ctxt = |
34d1913f0b20
clarified control antiquotations: decode control symbol to get name;
wenzelm
parents:
61471
diff
changeset
|
151 |
expand_src range |
34d1913f0b20
clarified control antiquotations: decode control symbol to get name;
wenzelm
parents:
61471
diff
changeset
|
152 |
(Token.read_antiq (Thy_Header.get_keywords' ctxt) antiq (body, #1 range)) ctxt; |
53167 | 153 |
|
27343
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
154 |
val ctxt = |
4b28b80dd1f8
add_antiq: more general notion of ML antiquotation;
wenzelm
parents:
26881
diff
changeset
|
155 |
(case opt_ctxt of |
48992 | 156 |
NONE => error ("No context -- cannot expand ML antiquotations" ^ Position.here pos) |
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
157 |
| SOME ctxt => struct_begin ctxt); |
27378 | 158 |
|
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
159 |
val (begin_env, end_env) = make_env (struct_name ctxt) visible; |
53167 | 160 |
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
|
161 |
val (ml_env, ml_body) = |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58991
diff
changeset
|
162 |
decls |> map (fn decl => decl ctxt') |> split_list |> apply2 flat; |
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
163 |
in ((begin_env @ ml_env @ end_env, ml_body), SOME ctxt') end; |
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
164 |
in ((ml_env, ml_body), opt_ctxt') end; |
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
165 |
|
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
166 |
in |
24574 | 167 |
|
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56229
diff
changeset
|
168 |
fun eval flags pos ants = |
24574 | 169 |
let |
56304
40274e4f5ebf
redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents:
56303
diff
changeset
|
170 |
val non_verbose = ML_Compiler.verbose false flags; |
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56229
diff
changeset
|
171 |
|
28270
7ada24ebea94
explicit handling of ML environment within generic context;
wenzelm
parents:
27895
diff
changeset
|
172 |
(*prepare source text*) |
41485
6c0de045d127
ML_trace: observe context visibility flag (import for Latex mode, for example);
wenzelm
parents:
41375
diff
changeset
|
173 |
val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ()); |
31334 | 174 |
val _ = |
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
175 |
(case env_ctxt of |
41485
6c0de045d127
ML_trace: observe context visibility flag (import for Latex mode, for example);
wenzelm
parents:
41375
diff
changeset
|
176 |
SOME ctxt => |
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56294
diff
changeset
|
177 |
if Config.get ctxt ML_Options.source_trace andalso Context_Position.is_visible ctxt |
56294
85911b8a6868
prefer Context_Position where a context is available;
wenzelm
parents:
56279
diff
changeset
|
178 |
then tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body]) |
41375 | 179 |
else () |
180 |
| NONE => ()); |
|
28270
7ada24ebea94
explicit handling of ML environment within generic context;
wenzelm
parents:
27895
diff
changeset
|
181 |
|
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
182 |
(*prepare environment*) |
41485
6c0de045d127
ML_trace: observe context visibility flag (import for Latex mode, for example);
wenzelm
parents:
41375
diff
changeset
|
183 |
val _ = |
6c0de045d127
ML_trace: observe context visibility flag (import for Latex mode, for example);
wenzelm
parents:
41375
diff
changeset
|
184 |
Context.setmp_thread_data |
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
185 |
(Option.map (Context.Proof o Context_Position.set_visible false) env_ctxt) |
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56229
diff
changeset
|
186 |
(fn () => (ML_Compiler.eval non_verbose Position.none env; Context.thread_data ())) () |
31325
700951b53d21
moved local ML environment to separate module ML_Env;
wenzelm
parents:
30683
diff
changeset
|
187 |
|> (fn NONE => () | SOME context' => Context.>> (ML_Env.inherit context')); |
28270
7ada24ebea94
explicit handling of ML environment within generic context;
wenzelm
parents:
27895
diff
changeset
|
188 |
|
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
189 |
(*eval body*) |
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56229
diff
changeset
|
190 |
val _ = ML_Compiler.eval flags pos body; |
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
191 |
|
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
192 |
(*clear environment*) |
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
193 |
val _ = |
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
194 |
(case (env_ctxt, is_some (Context.thread_data ())) of |
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
195 |
(SOME ctxt, true) => |
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
196 |
let |
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
197 |
val name = struct_name ctxt; |
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
198 |
val _ = ML_Compiler.eval non_verbose Position.none (reset_env name); |
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
199 |
val _ = Context.>> (ML_Env.forget_structure name); |
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
200 |
in () end |
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
201 |
| _ => ()); |
28270
7ada24ebea94
explicit handling of ML environment within generic context;
wenzelm
parents:
27895
diff
changeset
|
202 |
in () end; |
24574 | 203 |
|
204 |
end; |
|
205 |
||
206 |
||
30672
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents:
30643
diff
changeset
|
207 |
(* derived versions *) |
24574 | 208 |
|
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56229
diff
changeset
|
209 |
fun eval_file flags path = |
56203
76c72f4d0667
clarified bootstrap process: switch to ML with context and antiquotations earlier;
wenzelm
parents:
56201
diff
changeset
|
210 |
let val pos = Path.position path |
59067 | 211 |
in eval flags pos (ML_Lex.read_pos pos (File.read path)) end; |
56203
76c72f4d0667
clarified bootstrap process: switch to ML with context and antiquotations earlier;
wenzelm
parents:
56201
diff
changeset
|
212 |
|
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56229
diff
changeset
|
213 |
fun eval_source flags source = |
62873
2f9c8a18f832
support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;
wenzelm
parents:
62850
diff
changeset
|
214 |
eval flags (Input.pos_of source) (ML_Lex.read_source (#SML_syntax flags) 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
|
215 |
|
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56229
diff
changeset
|
216 |
fun eval_in ctxt flags 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
|
217 |
Context.setmp_thread_data (Option.map Context.Proof ctxt) |
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56229
diff
changeset
|
218 |
(fn () => eval flags pos ants) (); |
24574 | 219 |
|
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56229
diff
changeset
|
220 |
fun eval_source_in ctxt flags 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
|
221 |
Context.setmp_thread_data (Option.map Context.Proof ctxt) |
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56229
diff
changeset
|
222 |
(fn () => eval_source flags 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
|
223 |
|
58991
92b6f4e68c5a
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
58979
diff
changeset
|
224 |
fun expression range name constraint body ants = |
59067 | 225 |
exec (fn () => |
226 |
eval ML_Compiler.flags (#1 range) |
|
227 |
(ML_Lex.read "Context.set_thread_data (SOME (let val " @ ML_Lex.read_set_range range name @ |
|
228 |
ML_Lex.read (": " ^ constraint ^ " =") @ ants @ |
|
62876 | 229 |
ML_Lex.read ("in " ^ body ^ " end (Context.the_generic_context ())));"))); |
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
|
230 |
|
24574 | 231 |
end; |
232 |
||
62850 | 233 |
val ML = ML_Context.eval_source ML_Compiler.flags; |