author | wenzelm |
Mon, 20 Mar 2023 10:59:27 +0100 | |
changeset 77692 | 3e746e684f4b |
parent 77673 | 08fcde7c55c0 |
child 77776 | 58e53c61f15f |
permissions | -rw-r--r-- |
62355 | 1 |
(* Title: Pure/ML/ml_compiler.ML |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
3 |
|
62355 | 4 |
Runtime compilation and evaluation. |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
5 |
*) |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
6 |
|
62354 | 7 |
signature ML_COMPILER = |
8 |
sig |
|
9 |
type flags = |
|
68820
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68816
diff
changeset
|
10 |
{environment: string, redirect: bool, verbose: bool, |
62354 | 11 |
debug: bool option, writeln: string -> unit, warning: string -> unit} |
62490
39d01eaf5292
ML debugger support in Pure (again, see 3565c9f407ec);
wenzelm
parents:
62387
diff
changeset
|
12 |
val debug_flags: bool option -> flags |
62354 | 13 |
val flags: flags |
14 |
val verbose: bool -> flags -> flags |
|
15 |
val eval: flags -> Position.T -> ML_Lex.token list -> unit |
|
62490
39d01eaf5292
ML debugger support in Pure (again, see 3565c9f407ec);
wenzelm
parents:
62387
diff
changeset
|
16 |
end; |
62354 | 17 |
|
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
18 |
structure ML_Compiler: ML_COMPILER = |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
19 |
struct |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
20 |
|
62354 | 21 |
(* flags *) |
22 |
||
23 |
type flags = |
|
68820
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68816
diff
changeset
|
24 |
{environment: string, redirect: bool, verbose: bool, |
62354 | 25 |
debug: bool option, writeln: string -> unit, warning: string -> unit}; |
26 |
||
62490
39d01eaf5292
ML debugger support in Pure (again, see 3565c9f407ec);
wenzelm
parents:
62387
diff
changeset
|
27 |
fun debug_flags opt_debug : flags = |
68820
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68816
diff
changeset
|
28 |
{environment = "", redirect = false, verbose = false, |
62490
39d01eaf5292
ML debugger support in Pure (again, see 3565c9f407ec);
wenzelm
parents:
62387
diff
changeset
|
29 |
debug = opt_debug, writeln = writeln, warning = warning}; |
39d01eaf5292
ML debugger support in Pure (again, see 3565c9f407ec);
wenzelm
parents:
62387
diff
changeset
|
30 |
|
39d01eaf5292
ML debugger support in Pure (again, see 3565c9f407ec);
wenzelm
parents:
62387
diff
changeset
|
31 |
val flags = debug_flags NONE; |
62354 | 32 |
|
33 |
fun verbose b (flags: flags) = |
|
68820
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68816
diff
changeset
|
34 |
{environment = #environment flags, redirect = #redirect flags, verbose = b, |
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62889
diff
changeset
|
35 |
debug = #debug flags, writeln = #writeln flags, warning = #warning flags}; |
56281 | 36 |
|
37 |
||
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
38 |
(* parse trees *) |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
39 |
|
60913 | 40 |
fun breakpoint_position loc = |
62821 | 41 |
let val pos = Position.no_range_position (Exn_Properties.position_of_polyml_location loc) in |
60913 | 42 |
(case Position.offset_of pos of |
43 |
NONE => pos |
|
44 |
| SOME 1 => pos |
|
45 |
| SOME j => |
|
46 |
Position.properties_of pos |
|
63806 | 47 |
|> Properties.put (Markup.offsetN, Value.print_int (j - 1)) |
60913 | 48 |
|> Position.of_properties) |
49 |
end; |
|
50 |
||
62941 | 51 |
fun report_parse_tree redirect depth name_space parse_tree = |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
52 |
let |
71675 | 53 |
val reports_enabled = |
62889 | 54 |
(case Context.get_generic_context () of |
71675 | 55 |
SOME context => Context_Position.reports_enabled_generic context |
76804 | 56 |
| NONE => Context_Position.reports_enabled0 ()); |
71675 | 57 |
fun is_reported pos = reports_enabled andalso Position.is_reported pos; |
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
|
58 |
|
60744 | 59 |
|
60 |
(* syntax reports *) |
|
61 |
||
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
|
62 |
fun reported_types loc types = |
62821 | 63 |
let val pos = Exn_Properties.position_of_polyml_location loc in |
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
|
64 |
is_reported pos ? |
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
|
65 |
let |
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
|
66 |
val xml = |
62941 | 67 |
PolyML.NameSpace.Values.printType (types, depth, SOME name_space) |
62663 | 68 |
|> Pretty.from_polyml |> Pretty.string_of |
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
|
69 |
|> Output.output |> YXML.parse_body; |
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
|
70 |
in cons (pos, fn () => Markup.ML_typing, fn () => YXML.string_of_body xml) end |
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
|
71 |
end; |
38720
7f8bc335e203
ML_Context.eval: produce antiquotation environment preferably in invisible context, to avoid displaced report messages from ML_Compiler;
wenzelm
parents:
38228
diff
changeset
|
72 |
|
44737 | 73 |
fun reported_entity kind loc decl = |
58991
92b6f4e68c5a
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
56618
diff
changeset
|
74 |
let |
62821 | 75 |
val pos = Exn_Properties.position_of_polyml_location loc; |
76 |
val def_pos = Exn_Properties.position_of_polyml_location decl; |
|
58991
92b6f4e68c5a
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
56618
diff
changeset
|
77 |
in |
92b6f4e68c5a
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
56618
diff
changeset
|
78 |
(is_reported pos andalso pos <> def_pos) ? |
71910 | 79 |
cons (pos, fn () => Position.entity_markup kind ("", def_pos), fn () => "") |
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
|
80 |
end; |
41503
a7462e442e35
refined report_parse_tree: reverse reports happen to produce proper type information for inlined @{term}, @{typ} etc.;
wenzelm
parents:
41501
diff
changeset
|
81 |
|
62993 | 82 |
fun reported_entity_id def id loc = |
83 |
let |
|
84 |
val pos = Exn_Properties.position_of_polyml_location loc; |
|
85 |
in |
|
64661 | 86 |
(is_reported pos andalso id <> 0) ? |
62993 | 87 |
let |
88 |
fun markup () = |
|
63806 | 89 |
(Markup.entityN, [(if def then Markup.defN else Markup.refN, Value.print_int id)]); |
62993 | 90 |
in cons (pos, markup, fn () => "") end |
91 |
end; |
|
92 |
||
60731
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
60730
diff
changeset
|
93 |
fun reported_completions loc names = |
62821 | 94 |
let val pos = Exn_Properties.position_of_polyml_location loc in |
60732 | 95 |
if is_reported pos andalso not (null names) then |
60731
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
60730
diff
changeset
|
96 |
let |
60732 | 97 |
val completion = Completion.names pos (map (fn a => (a, ("ML", a))) names); |
60731
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
60730
diff
changeset
|
98 |
val xml = Completion.encode completion; |
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
60730
diff
changeset
|
99 |
in cons (pos, fn () => Markup.completion, fn () => YXML.string_of_body xml) end |
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
60730
diff
changeset
|
100 |
else I |
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
60730
diff
changeset
|
101 |
end; |
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
60730
diff
changeset
|
102 |
|
60744 | 103 |
fun reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ()) |
104 |
| reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ()) |
|
62993 | 105 |
| reported loc (PolyML.PTdefId id) = reported_entity_id true (FixedInt.toLarge id) loc |
106 |
| reported loc (PolyML.PTrefId id) = reported_entity_id false (FixedInt.toLarge id) loc |
|
60744 | 107 |
| reported loc (PolyML.PTtype types) = reported_types loc types |
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
|
108 |
| reported loc (PolyML.PTdeclaredAt decl) = reported_entity Markup.ML_defN loc decl |
62501 | 109 |
| reported loc (PolyML.PTcompletions names) = reported_completions loc names |
110 |
| reported _ _ = I |
|
44737 | 111 |
and reported_tree (loc, props) = fold (reported loc) props; |
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
|
112 |
|
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
|
113 |
val persistent_reports = reported_tree parse_tree []; |
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
|
114 |
|
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
|
115 |
fun output () = |
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
|
116 |
persistent_reports |
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
|
117 |
|> map (fn (pos, markup, text) => Position.reported_text pos (markup ()) (text ())) |
56333
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
56305
diff
changeset
|
118 |
|> Output.report; |
60744 | 119 |
val _ = |
72825 | 120 |
if not (null persistent_reports) andalso redirect andalso |
77673
08fcde7c55c0
clarified ML option vs. Scala option (see also caa182bdab7a);
wenzelm
parents:
76804
diff
changeset
|
121 |
not (Options.default_bool "pide_reports") andalso Future.enabled () |
60744 | 122 |
then |
123 |
Execution.print |
|
124 |
{name = "ML_Compiler.report", pos = Position.thread_data (), pri = Task_Queue.urgent_pri} |
|
125 |
output |
|
126 |
else output (); |
|
127 |
||
128 |
||
129 |
(* breakpoints *) |
|
130 |
||
131 |
fun breakpoints _ (PolyML.PTnextSibling tree) = breakpoints_tree (tree ()) |
|
132 |
| breakpoints _ (PolyML.PTfirstChild tree) = breakpoints_tree (tree ()) |
|
62501 | 133 |
| breakpoints loc (PolyML.PTbreakPoint b) = |
134 |
let val pos = breakpoint_position loc in |
|
135 |
if is_reported pos then |
|
136 |
let val id = serial (); |
|
137 |
in cons ((pos, Markup.ML_breakpoint id), (id, (b, pos))) end |
|
138 |
else I |
|
139 |
end |
|
140 |
| breakpoints _ _ = I |
|
60744 | 141 |
and breakpoints_tree (loc, props) = fold (breakpoints loc) props; |
142 |
||
143 |
val all_breakpoints = rev (breakpoints_tree parse_tree []); |
|
144 |
val _ = Position.reports (map #1 all_breakpoints); |
|
62941 | 145 |
in map (fn (_, (id, (b, pos))) => (id, (b, Position.dest pos))) all_breakpoints end; |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
146 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
147 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
148 |
(* eval ML source tokens *) |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
149 |
|
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
|
150 |
fun eval (flags: flags) pos toks = |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
151 |
let |
62889 | 152 |
val opt_context = Context.get_generic_context (); |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
153 |
|
62941 | 154 |
val env as {debug, name_space, add_breakpoints} = |
68820
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68816
diff
changeset
|
155 |
(case (ML_Recursive.get (), #environment flags <> "") of |
62941 | 156 |
(SOME env, false) => env |
157 |
| _ => |
|
68820
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68816
diff
changeset
|
158 |
{debug = |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68816
diff
changeset
|
159 |
(case #debug flags of |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68816
diff
changeset
|
160 |
SOME debug => debug |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68816
diff
changeset
|
161 |
| NONE => ML_Options.debugger_enabled opt_context), |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68816
diff
changeset
|
162 |
name_space = ML_Env.make_name_space (#environment flags), |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68816
diff
changeset
|
163 |
add_breakpoints = ML_Env.add_breakpoints}); |
62941 | 164 |
|
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
165 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
166 |
(* input *) |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
167 |
|
50911
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
50910
diff
changeset
|
168 |
val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos))); |
31437 | 169 |
|
68821
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
170 |
val {explode_token, ...} = ML_Env.operations opt_context (#environment flags); |
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
171 |
fun token_content tok = if ML_Lex.is_comment tok then NONE else SOME (`explode_token tok); |
67362 | 172 |
|
41501
b5ad6b0d6d7c
ML compiler: more careful treatment of input tokens -- trailing space ensures proper separation and end position (cf. 82c1e348bc18, 08240feb69c7);
wenzelm
parents:
41484
diff
changeset
|
173 |
val input_buffer = |
67362 | 174 |
Unsynchronized.ref (map_filter token_content toks); |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
175 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
176 |
fun get () = |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
177 |
(case ! input_buffer of |
41501
b5ad6b0d6d7c
ML compiler: more careful treatment of input tokens -- trailing space ensures proper separation and end position (cf. 82c1e348bc18, 08240feb69c7);
wenzelm
parents:
41484
diff
changeset
|
178 |
(c :: cs, tok) :: rest => (input_buffer := (cs, tok) :: rest; SOME c) |
b5ad6b0d6d7c
ML compiler: more careful treatment of input tokens -- trailing space ensures proper separation and end position (cf. 82c1e348bc18, 08240feb69c7);
wenzelm
parents:
41484
diff
changeset
|
179 |
| ([], _) :: rest => (input_buffer := rest; SOME #" ") |
b5ad6b0d6d7c
ML compiler: more careful treatment of input tokens -- trailing space ensures proper separation and end position (cf. 82c1e348bc18, 08240feb69c7);
wenzelm
parents:
41484
diff
changeset
|
180 |
| [] => NONE); |
b5ad6b0d6d7c
ML compiler: more careful treatment of input tokens -- trailing space ensures proper separation and end position (cf. 82c1e348bc18, 08240feb69c7);
wenzelm
parents:
41484
diff
changeset
|
181 |
|
b5ad6b0d6d7c
ML compiler: more careful treatment of input tokens -- trailing space ensures proper separation and end position (cf. 82c1e348bc18, 08240feb69c7);
wenzelm
parents:
41484
diff
changeset
|
182 |
fun get_pos () = |
b5ad6b0d6d7c
ML compiler: more careful treatment of input tokens -- trailing space ensures proper separation and end position (cf. 82c1e348bc18, 08240feb69c7);
wenzelm
parents:
41484
diff
changeset
|
183 |
(case ! input_buffer of |
b5ad6b0d6d7c
ML compiler: more careful treatment of input tokens -- trailing space ensures proper separation and end position (cf. 82c1e348bc18, 08240feb69c7);
wenzelm
parents:
41484
diff
changeset
|
184 |
(_ :: _, tok) :: _ => ML_Lex.pos_of tok |
b5ad6b0d6d7c
ML compiler: more careful treatment of input tokens -- trailing space ensures proper separation and end position (cf. 82c1e348bc18, 08240feb69c7);
wenzelm
parents:
41484
diff
changeset
|
185 |
| ([], tok) :: _ => ML_Lex.end_pos_of tok |
b5ad6b0d6d7c
ML compiler: more careful treatment of input tokens -- trailing space ensures proper separation and end position (cf. 82c1e348bc18, 08240feb69c7);
wenzelm
parents:
41484
diff
changeset
|
186 |
| [] => Position.none); |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
187 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
188 |
|
60744 | 189 |
(* output *) |
39228
cb7264721c91
ML_Compiler.eval: more careful printing of messages and regular output, trying to accomodate Poly/ML, Proof General, Isabelle/Scala/jEdit at the same time;
wenzelm
parents:
39227
diff
changeset
|
190 |
|
cb7264721c91
ML_Compiler.eval: more careful printing of messages and regular output, trying to accomodate Poly/ML, Proof General, Isabelle/Scala/jEdit at the same time;
wenzelm
parents:
39227
diff
changeset
|
191 |
val writeln_buffer = Unsynchronized.ref Buffer.empty; |
cb7264721c91
ML_Compiler.eval: more careful printing of messages and regular output, trying to accomodate Poly/ML, Proof General, Isabelle/Scala/jEdit at the same time;
wenzelm
parents:
39227
diff
changeset
|
192 |
fun write s = Unsynchronized.change writeln_buffer (Buffer.add s); |
60858 | 193 |
fun output_writeln () = #writeln flags (trim_line (Buffer.content (! writeln_buffer))); |
39228
cb7264721c91
ML_Compiler.eval: more careful printing of messages and regular output, trying to accomodate Poly/ML, Proof General, Isabelle/Scala/jEdit at the same time;
wenzelm
parents:
39227
diff
changeset
|
194 |
|
cb7264721c91
ML_Compiler.eval: more careful printing of messages and regular output, trying to accomodate Poly/ML, Proof General, Isabelle/Scala/jEdit at the same time;
wenzelm
parents:
39227
diff
changeset
|
195 |
val warnings = Unsynchronized.ref ([]: string list); |
39231
25c345302a17
avoid mixing of static and runtime errors in compiler output, to accomodate Proof General;
wenzelm
parents:
39230
diff
changeset
|
196 |
fun warn msg = Unsynchronized.change warnings (cons msg); |
60858 | 197 |
fun output_warnings () = List.app (#warning flags) (rev (! warnings)); |
39228
cb7264721c91
ML_Compiler.eval: more careful printing of messages and regular output, trying to accomodate Poly/ML, Proof General, Isabelle/Scala/jEdit at the same time;
wenzelm
parents:
39227
diff
changeset
|
198 |
|
cb7264721c91
ML_Compiler.eval: more careful printing of messages and regular output, trying to accomodate Poly/ML, Proof General, Isabelle/Scala/jEdit at the same time;
wenzelm
parents:
39227
diff
changeset
|
199 |
val error_buffer = Unsynchronized.ref Buffer.empty; |
39231
25c345302a17
avoid mixing of static and runtime errors in compiler output, to accomodate Proof General;
wenzelm
parents:
39230
diff
changeset
|
200 |
fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n"); |
60872 | 201 |
fun flush_error () = #writeln flags (trim_line (Buffer.content (! error_buffer))); |
202 |
fun raise_error msg = error (trim_line (Buffer.content (Buffer.add msg (! error_buffer)))); |
|
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
203 |
|
39228
cb7264721c91
ML_Compiler.eval: more careful printing of messages and regular output, trying to accomodate Poly/ML, Proof General, Isabelle/Scala/jEdit at the same time;
wenzelm
parents:
39227
diff
changeset
|
204 |
fun message {message = msg, hard, location = loc, context = _} = |
cb7264721c91
ML_Compiler.eval: more careful printing of messages and regular output, trying to accomodate Poly/ML, Proof General, Isabelle/Scala/jEdit at the same time;
wenzelm
parents:
39227
diff
changeset
|
205 |
let |
62821 | 206 |
val pos = Exn_Properties.position_of_polyml_location loc; |
39228
cb7264721c91
ML_Compiler.eval: more careful printing of messages and regular output, trying to accomodate Poly/ML, Proof General, Isabelle/Scala/jEdit at the same time;
wenzelm
parents:
39227
diff
changeset
|
207 |
val txt = |
49828
5631ee099293
more basic ML compiler messages -- avoid conflict of 638cefe3ee99 and cb7264721c91 concerning Protocol.message_positions;
wenzelm
parents:
48992
diff
changeset
|
208 |
(if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^ |
62663 | 209 |
Pretty.string_of (Pretty.from_polyml msg); |
39231
25c345302a17
avoid mixing of static and runtime errors in compiler output, to accomodate Proof General;
wenzelm
parents:
39230
diff
changeset
|
210 |
in if hard then err txt else warn txt end; |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
211 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
212 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
213 |
(* results *) |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
214 |
|
62878 | 215 |
val depth = FixedInt.fromInt (ML_Print_Depth.get_print_depth ()); |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
216 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
217 |
fun apply_result {fixes, types, signatures, structures, functors, values} = |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
218 |
let |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
219 |
fun display disp x = |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
220 |
if depth > 0 then |
62663 | 221 |
(write (disp x |> Pretty.from_polyml |> Pretty.string_of); write "\n") |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
222 |
else (); |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
223 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
224 |
fun apply_fix (a, b) = |
62941 | 225 |
(#enterFix name_space (a, b); |
226 |
display PolyML.NameSpace.Infixes.print b); |
|
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
227 |
fun apply_type (a, b) = |
62941 | 228 |
(#enterType name_space (a, b); |
229 |
display PolyML.NameSpace.TypeConstrs.print (b, depth, SOME name_space)); |
|
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
230 |
fun apply_sig (a, b) = |
62941 | 231 |
(#enterSig name_space (a, b); |
232 |
display PolyML.NameSpace.Signatures.print (b, depth, SOME name_space)); |
|
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
233 |
fun apply_struct (a, b) = |
62941 | 234 |
(#enterStruct name_space (a, b); |
235 |
display PolyML.NameSpace.Structures.print (b, depth, SOME name_space)); |
|
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
236 |
fun apply_funct (a, b) = |
62941 | 237 |
(#enterFunct name_space (a, b); |
238 |
display PolyML.NameSpace.Functors.print (b, depth, SOME name_space)); |
|
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
239 |
fun apply_val (a, b) = |
62941 | 240 |
(#enterVal name_space (a, b); |
241 |
display PolyML.NameSpace.Values.printWithType (b, depth, SOME name_space)); |
|
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
242 |
in |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
243 |
List.app apply_fix fixes; |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
244 |
List.app apply_type types; |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
245 |
List.app apply_sig signatures; |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
246 |
List.app apply_struct structures; |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
247 |
List.app apply_funct functors; |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
248 |
List.app apply_val values |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
249 |
end; |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
250 |
|
39231
25c345302a17
avoid mixing of static and runtime errors in compiler output, to accomodate Proof General;
wenzelm
parents:
39230
diff
changeset
|
251 |
exception STATIC_ERRORS of unit; |
39230
184507f6e8d0
ML_Compiler.eval: discontinued extra "Static Errors" of raw Poly/ML;
wenzelm
parents:
39228
diff
changeset
|
252 |
|
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
253 |
fun result_fun (phase1, phase2) () = |
31477 | 254 |
((case phase1 of |
255 |
NONE => () |
|
62941 | 256 |
| SOME parse_tree => |
257 |
add_breakpoints (report_parse_tree (#redirect flags) depth name_space parse_tree)); |
|
31477 | 258 |
(case phase2 of |
39231
25c345302a17
avoid mixing of static and runtime errors in compiler output, to accomodate Proof General;
wenzelm
parents:
39230
diff
changeset
|
259 |
NONE => raise STATIC_ERRORS () |
31477 | 260 |
| SOME code => |
33603
3713a5208671
generalized Runtime.toplevel_error wrt. output function;
wenzelm
parents:
33538
diff
changeset
|
261 |
apply_result |
3713a5208671
generalized Runtime.toplevel_error wrt. output function;
wenzelm
parents:
33538
diff
changeset
|
262 |
((code |
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56281
diff
changeset
|
263 |
|> Runtime.debugging opt_context |
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56281
diff
changeset
|
264 |
|> Runtime.toplevel_error (err o Runtime.exn_message)) ()))); |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
265 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
266 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
267 |
(* compiler invocation *) |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
268 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
269 |
val parameters = |
39228
cb7264721c91
ML_Compiler.eval: more careful printing of messages and regular output, trying to accomodate Poly/ML, Proof General, Isabelle/Scala/jEdit at the same time;
wenzelm
parents:
39227
diff
changeset
|
270 |
[PolyML.Compiler.CPOutStream write, |
62941 | 271 |
PolyML.Compiler.CPNameSpace name_space, |
39228
cb7264721c91
ML_Compiler.eval: more careful printing of messages and regular output, trying to accomodate Poly/ML, Proof General, Isabelle/Scala/jEdit at the same time;
wenzelm
parents:
39227
diff
changeset
|
272 |
PolyML.Compiler.CPErrorMessageProc message, |
41501
b5ad6b0d6d7c
ML compiler: more careful treatment of input tokens -- trailing space ensures proper separation and end position (cf. 82c1e348bc18, 08240feb69c7);
wenzelm
parents:
41484
diff
changeset
|
273 |
PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos), |
b5ad6b0d6d7c
ML compiler: more careful treatment of input tokens -- trailing space ensures proper separation and end position (cf. 82c1e348bc18, 08240feb69c7);
wenzelm
parents:
41484
diff
changeset
|
274 |
PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos), |
31437 | 275 |
PolyML.Compiler.CPFileName location_props, |
62878 | 276 |
PolyML.Compiler.CPPrintDepth ML_Print_Depth.get_print_depth, |
31475 | 277 |
PolyML.Compiler.CPCompilerResultFun result_fun, |
62501 | 278 |
PolyML.Compiler.CPPrintInAlphabeticalOrder false, |
62993 | 279 |
PolyML.Compiler.CPDebug debug, |
280 |
PolyML.Compiler.CPBindingSeq serial]; |
|
60956 | 281 |
|
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
282 |
val _ = |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
283 |
(while not (List.null (! input_buffer)) do |
62941 | 284 |
ML_Recursive.recursive env (fn () => PolyML.compiler (get, parameters) ())) |
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
285 |
handle exn => |
62505 | 286 |
if Exn.is_interrupt exn then Exn.reraise exn |
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
287 |
else |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
288 |
let |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
289 |
val exn_msg = |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
290 |
(case exn of |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
291 |
STATIC_ERRORS () => "" |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
292 |
| Runtime.TOPLEVEL_ERROR => "" |
62516 | 293 |
| _ => "Exception- " ^ Pretty.string_of (Runtime.pretty_exn exn) ^ " raised"); |
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
294 |
val _ = output_warnings (); |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
295 |
val _ = output_writeln (); |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
296 |
in raise_error exn_msg end; |
39228
cb7264721c91
ML_Compiler.eval: more careful printing of messages and regular output, trying to accomodate Poly/ML, Proof General, Isabelle/Scala/jEdit at the same time;
wenzelm
parents:
39227
diff
changeset
|
297 |
in |
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
|
298 |
if #verbose flags then (output_warnings (); flush_error (); output_writeln ()) |
39228
cb7264721c91
ML_Compiler.eval: more careful printing of messages and regular output, trying to accomodate Poly/ML, Proof General, Isabelle/Scala/jEdit at the same time;
wenzelm
parents:
39227
diff
changeset
|
299 |
else () |
cb7264721c91
ML_Compiler.eval: more careful printing of messages and regular output, trying to accomodate Poly/ML, Proof General, Isabelle/Scala/jEdit at the same time;
wenzelm
parents:
39227
diff
changeset
|
300 |
end; |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
301 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
302 |
end; |