author | paulson <lp15@cam.ac.uk> |
Sun, 12 May 2024 23:23:39 +0100 | |
changeset 80176 | 7fefa7839ac6 |
parent 78759 | 461e924cc825 |
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 = |
|
78728
72631efa3821
explicitly reject 'handle' with catch-all patterns;
wenzelm
parents:
78724
diff
changeset
|
10 |
{environment: string, redirect: bool, verbose: bool, catch_all: 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 |
|
78728
72631efa3821
explicitly reject 'handle' with catch-all patterns;
wenzelm
parents:
78724
diff
changeset
|
15 |
val ML_catch_all: bool Config.T |
62354 | 16 |
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
|
17 |
end; |
62354 | 18 |
|
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
19 |
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
|
20 |
struct |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
21 |
|
62354 | 22 |
(* flags *) |
23 |
||
24 |
type flags = |
|
78728
72631efa3821
explicitly reject 'handle' with catch-all patterns;
wenzelm
parents:
78724
diff
changeset
|
25 |
{environment: string, redirect: bool, verbose: bool, catch_all: bool, |
62354 | 26 |
debug: bool option, writeln: string -> unit, warning: string -> unit}; |
27 |
||
62490
39d01eaf5292
ML debugger support in Pure (again, see 3565c9f407ec);
wenzelm
parents:
62387
diff
changeset
|
28 |
fun debug_flags opt_debug : flags = |
78728
72631efa3821
explicitly reject 'handle' with catch-all patterns;
wenzelm
parents:
78724
diff
changeset
|
29 |
{environment = "", redirect = false, verbose = false, catch_all = false, |
62490
39d01eaf5292
ML debugger support in Pure (again, see 3565c9f407ec);
wenzelm
parents:
62387
diff
changeset
|
30 |
debug = opt_debug, writeln = writeln, warning = warning}; |
39d01eaf5292
ML debugger support in Pure (again, see 3565c9f407ec);
wenzelm
parents:
62387
diff
changeset
|
31 |
|
39d01eaf5292
ML debugger support in Pure (again, see 3565c9f407ec);
wenzelm
parents:
62387
diff
changeset
|
32 |
val flags = debug_flags NONE; |
62354 | 33 |
|
78728
72631efa3821
explicitly reject 'handle' with catch-all patterns;
wenzelm
parents:
78724
diff
changeset
|
34 |
fun verbose b ({environment, redirect, verbose = _, catch_all, debug, writeln, warning}: flags) = |
72631efa3821
explicitly reject 'handle' with catch-all patterns;
wenzelm
parents:
78724
diff
changeset
|
35 |
{environment = environment, redirect = redirect, verbose = b, catch_all = catch_all, |
72631efa3821
explicitly reject 'handle' with catch-all patterns;
wenzelm
parents:
78724
diff
changeset
|
36 |
debug = debug, writeln = writeln, warning = warning}; |
56281 | 37 |
|
38 |
||
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
39 |
(* parse trees *) |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
40 |
|
60913 | 41 |
fun breakpoint_position loc = |
62821 | 42 |
let val pos = Position.no_range_position (Exn_Properties.position_of_polyml_location loc) in |
60913 | 43 |
(case Position.offset_of pos of |
44 |
NONE => pos |
|
45 |
| SOME 1 => pos |
|
46 |
| SOME j => |
|
47 |
Position.properties_of pos |
|
63806 | 48 |
|> Properties.put (Markup.offsetN, Value.print_int (j - 1)) |
60913 | 49 |
|> Position.of_properties) |
50 |
end; |
|
51 |
||
62941 | 52 |
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
|
53 |
let |
71675 | 54 |
val reports_enabled = |
62889 | 55 |
(case Context.get_generic_context () of |
71675 | 56 |
SOME context => Context_Position.reports_enabled_generic context |
76804 | 57 |
| NONE => Context_Position.reports_enabled0 ()); |
71675 | 58 |
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
|
59 |
|
60744 | 60 |
|
61 |
(* syntax reports *) |
|
62 |
||
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
|
63 |
fun reported_types loc types = |
62821 | 64 |
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
|
65 |
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
|
66 |
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
|
67 |
val xml = |
62941 | 68 |
PolyML.NameSpace.Values.printType (types, depth, SOME name_space) |
62663 | 69 |
|> 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
|
70 |
|> 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
|
71 |
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
|
72 |
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
|
73 |
|
44737 | 74 |
fun reported_entity kind loc decl = |
58991
92b6f4e68c5a
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
56618
diff
changeset
|
75 |
let |
62821 | 76 |
val pos = Exn_Properties.position_of_polyml_location loc; |
77 |
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
|
78 |
in |
92b6f4e68c5a
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
56618
diff
changeset
|
79 |
(is_reported pos andalso pos <> def_pos) ? |
71910 | 80 |
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
|
81 |
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
|
82 |
|
62993 | 83 |
fun reported_entity_id def id loc = |
84 |
let |
|
85 |
val pos = Exn_Properties.position_of_polyml_location loc; |
|
86 |
in |
|
64661 | 87 |
(is_reported pos andalso id <> 0) ? |
62993 | 88 |
let |
89 |
fun markup () = |
|
63806 | 90 |
(Markup.entityN, [(if def then Markup.defN else Markup.refN, Value.print_int id)]); |
62993 | 91 |
in cons (pos, markup, fn () => "") end |
92 |
end; |
|
93 |
||
60731
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
60730
diff
changeset
|
94 |
fun reported_completions loc names = |
62821 | 95 |
let val pos = Exn_Properties.position_of_polyml_location loc in |
60732 | 96 |
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
|
97 |
let |
60732 | 98 |
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
|
99 |
val xml = Completion.encode completion; |
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
60730
diff
changeset
|
100 |
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
|
101 |
else I |
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
60730
diff
changeset
|
102 |
end; |
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
60730
diff
changeset
|
103 |
|
60744 | 104 |
fun reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ()) |
105 |
| reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ()) |
|
62993 | 106 |
| reported loc (PolyML.PTdefId id) = reported_entity_id true (FixedInt.toLarge id) loc |
107 |
| reported loc (PolyML.PTrefId id) = reported_entity_id false (FixedInt.toLarge id) loc |
|
60744 | 108 |
| 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
|
109 |
| reported loc (PolyML.PTdeclaredAt decl) = reported_entity Markup.ML_defN loc decl |
62501 | 110 |
| reported loc (PolyML.PTcompletions names) = reported_completions loc names |
111 |
| reported _ _ = I |
|
44737 | 112 |
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
|
113 |
|
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 |
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
|
115 |
|
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 |
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
|
117 |
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
|
118 |
|> 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
|
119 |
|> Output.report; |
60744 | 120 |
val _ = |
72825 | 121 |
if not (null persistent_reports) andalso redirect andalso |
77673
08fcde7c55c0
clarified ML option vs. Scala option (see also caa182bdab7a);
wenzelm
parents:
76804
diff
changeset
|
122 |
not (Options.default_bool "pide_reports") andalso Future.enabled () |
60744 | 123 |
then |
124 |
Execution.print |
|
125 |
{name = "ML_Compiler.report", pos = Position.thread_data (), pri = Task_Queue.urgent_pri} |
|
126 |
output |
|
127 |
else output (); |
|
128 |
||
129 |
||
130 |
(* breakpoints *) |
|
131 |
||
132 |
fun breakpoints _ (PolyML.PTnextSibling tree) = breakpoints_tree (tree ()) |
|
133 |
| breakpoints _ (PolyML.PTfirstChild tree) = breakpoints_tree (tree ()) |
|
62501 | 134 |
| breakpoints loc (PolyML.PTbreakPoint b) = |
135 |
let val pos = breakpoint_position loc in |
|
136 |
if is_reported pos then |
|
137 |
let val id = serial (); |
|
138 |
in cons ((pos, Markup.ML_breakpoint id), (id, (b, pos))) end |
|
139 |
else I |
|
140 |
end |
|
141 |
| breakpoints _ _ = I |
|
60744 | 142 |
and breakpoints_tree (loc, props) = fold (breakpoints loc) props; |
143 |
||
144 |
val all_breakpoints = rev (breakpoints_tree parse_tree []); |
|
145 |
val _ = Position.reports (map #1 all_breakpoints); |
|
62941 | 146 |
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
|
147 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
148 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
149 |
(* 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
|
150 |
|
78728
72631efa3821
explicitly reject 'handle' with catch-all patterns;
wenzelm
parents:
78724
diff
changeset
|
151 |
val ML_catch_all = Config.declare_bool ("ML_catch_all", \<^here>) (K false); |
72631efa3821
explicitly reject 'handle' with catch-all patterns;
wenzelm
parents:
78724
diff
changeset
|
152 |
|
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
|
153 |
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
|
154 |
let |
62889 | 155 |
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
|
156 |
|
62941 | 157 |
val env as {debug, name_space, add_breakpoints} = |
68820
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68816
diff
changeset
|
158 |
(case (ML_Recursive.get (), #environment flags <> "") of |
62941 | 159 |
(SOME env, false) => env |
160 |
| _ => |
|
68820
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68816
diff
changeset
|
161 |
{debug = |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68816
diff
changeset
|
162 |
(case #debug flags of |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68816
diff
changeset
|
163 |
SOME debug => debug |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68816
diff
changeset
|
164 |
| NONE => ML_Options.debugger_enabled opt_context), |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68816
diff
changeset
|
165 |
name_space = ML_Env.make_name_space (#environment flags), |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68816
diff
changeset
|
166 |
add_breakpoints = ML_Env.add_breakpoints}); |
62941 | 167 |
|
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
168 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
169 |
(* input *) |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
170 |
|
77776 | 171 |
val position_props = |
78021 | 172 |
filter (fn (a, _) => a = Markup.labelN orelse a = Markup.fileN orelse a = Markup.idN) |
173 |
(Position.properties_of pos); |
|
77776 | 174 |
val location_props = op ^ (YXML.output_markup (":", position_props)); |
31437 | 175 |
|
68821
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
176 |
val {explode_token, ...} = ML_Env.operations opt_context (#environment flags); |
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
177 |
fun token_content tok = if ML_Lex.is_comment tok then NONE else SOME (`explode_token tok); |
67362 | 178 |
|
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
|
179 |
val input_buffer = |
67362 | 180 |
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
|
181 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
182 |
fun get () = |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
183 |
(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
|
184 |
(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
|
185 |
| ([], _) :: 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
|
186 |
| [] => 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
|
187 |
|
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
|
188 |
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
|
189 |
(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
|
190 |
(_ :: _, 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
|
191 |
| ([], 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
|
192 |
| [] => 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
|
193 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
194 |
|
60744 | 195 |
(* 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
|
196 |
|
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
|
197 |
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
|
198 |
fun write s = Unsynchronized.change writeln_buffer (Buffer.add s); |
60858 | 199 |
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
|
200 |
|
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
|
201 |
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
|
202 |
fun warn msg = Unsynchronized.change warnings (cons msg); |
60858 | 203 |
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
|
204 |
|
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 |
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
|
206 |
fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n"); |
78724
f2d7f4334cdc
clarified output vs. error: presence of error messages means error (see also cb7264721c91);
wenzelm
parents:
78021
diff
changeset
|
207 |
|
f2d7f4334cdc
clarified output vs. error: presence of error messages means error (see also cb7264721c91);
wenzelm
parents:
78021
diff
changeset
|
208 |
fun expose_error verbose = |
f2d7f4334cdc
clarified output vs. error: presence of error messages means error (see also cb7264721c91);
wenzelm
parents:
78021
diff
changeset
|
209 |
let |
f2d7f4334cdc
clarified output vs. error: presence of error messages means error (see also cb7264721c91);
wenzelm
parents:
78021
diff
changeset
|
210 |
val msg = Buffer.content (! error_buffer); |
f2d7f4334cdc
clarified output vs. error: presence of error messages means error (see also cb7264721c91);
wenzelm
parents:
78021
diff
changeset
|
211 |
val is_err = msg <> ""; |
f2d7f4334cdc
clarified output vs. error: presence of error messages means error (see also cb7264721c91);
wenzelm
parents:
78021
diff
changeset
|
212 |
val _ = if is_err orelse verbose then (output_warnings (); output_writeln ()) else (); |
f2d7f4334cdc
clarified output vs. error: presence of error messages means error (see also cb7264721c91);
wenzelm
parents:
78021
diff
changeset
|
213 |
in if is_err then error (trim_line msg) else () end; |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
214 |
|
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
|
215 |
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
|
216 |
let |
62821 | 217 |
val pos = Exn_Properties.position_of_polyml_location loc; |
78728
72631efa3821
explicitly reject 'handle' with catch-all patterns;
wenzelm
parents:
78724
diff
changeset
|
218 |
val s = Pretty.string_of (Pretty.from_polyml msg); |
72631efa3821
explicitly reject 'handle' with catch-all patterns;
wenzelm
parents:
78724
diff
changeset
|
219 |
val catch_all = |
72631efa3821
explicitly reject 'handle' with catch-all patterns;
wenzelm
parents:
78724
diff
changeset
|
220 |
#catch_all flags orelse |
72631efa3821
explicitly reject 'handle' with catch-all patterns;
wenzelm
parents:
78724
diff
changeset
|
221 |
(case opt_context of |
72631efa3821
explicitly reject 'handle' with catch-all patterns;
wenzelm
parents:
78724
diff
changeset
|
222 |
NONE => false |
72631efa3821
explicitly reject 'handle' with catch-all patterns;
wenzelm
parents:
78724
diff
changeset
|
223 |
| SOME context => Config.get_generic context ML_catch_all); |
72631efa3821
explicitly reject 'handle' with catch-all patterns;
wenzelm
parents:
78724
diff
changeset
|
224 |
val is_err = |
72631efa3821
explicitly reject 'handle' with catch-all patterns;
wenzelm
parents:
78724
diff
changeset
|
225 |
hard orelse |
72631efa3821
explicitly reject 'handle' with catch-all patterns;
wenzelm
parents:
78724
diff
changeset
|
226 |
(not catch_all andalso |
72631efa3821
explicitly reject 'handle' with catch-all patterns;
wenzelm
parents:
78724
diff
changeset
|
227 |
String.isPrefix "Handler catches all exceptions" (XML.content_of (YXML.parse_body s))); |
72631efa3821
explicitly reject 'handle' with catch-all patterns;
wenzelm
parents:
78724
diff
changeset
|
228 |
val txt = (if is_err then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^ s; |
72631efa3821
explicitly reject 'handle' with catch-all patterns;
wenzelm
parents:
78724
diff
changeset
|
229 |
in if is_err 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
|
230 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
231 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
232 |
(* results *) |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
233 |
|
62878 | 234 |
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
|
235 |
|
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_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
|
237 |
let |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
238 |
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
|
239 |
if depth > 0 then |
62663 | 240 |
(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
|
241 |
else (); |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
242 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
243 |
fun apply_fix (a, b) = |
62941 | 244 |
(#enterFix name_space (a, b); |
245 |
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
|
246 |
fun apply_type (a, b) = |
62941 | 247 |
(#enterType name_space (a, b); |
248 |
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
|
249 |
fun apply_sig (a, b) = |
62941 | 250 |
(#enterSig name_space (a, b); |
251 |
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
|
252 |
fun apply_struct (a, b) = |
62941 | 253 |
(#enterStruct name_space (a, b); |
254 |
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
|
255 |
fun apply_funct (a, b) = |
62941 | 256 |
(#enterFunct name_space (a, b); |
257 |
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
|
258 |
fun apply_val (a, b) = |
62941 | 259 |
(#enterVal name_space (a, b); |
260 |
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
|
261 |
in |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
262 |
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
|
263 |
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
|
264 |
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
|
265 |
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
|
266 |
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
|
267 |
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
|
268 |
end; |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
269 |
|
39231
25c345302a17
avoid mixing of static and runtime errors in compiler output, to accomodate Proof General;
wenzelm
parents:
39230
diff
changeset
|
270 |
exception STATIC_ERRORS of unit; |
39230
184507f6e8d0
ML_Compiler.eval: discontinued extra "Static Errors" of raw Poly/ML;
wenzelm
parents:
39228
diff
changeset
|
271 |
|
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
272 |
fun result_fun (phase1, phase2) () = |
31477 | 273 |
((case phase1 of |
274 |
NONE => () |
|
62941 | 275 |
| SOME parse_tree => |
276 |
add_breakpoints (report_parse_tree (#redirect flags) depth name_space parse_tree)); |
|
31477 | 277 |
(case phase2 of |
39231
25c345302a17
avoid mixing of static and runtime errors in compiler output, to accomodate Proof General;
wenzelm
parents:
39230
diff
changeset
|
278 |
NONE => raise STATIC_ERRORS () |
31477 | 279 |
| SOME code => |
33603
3713a5208671
generalized Runtime.toplevel_error wrt. output function;
wenzelm
parents:
33538
diff
changeset
|
280 |
apply_result |
3713a5208671
generalized Runtime.toplevel_error wrt. output function;
wenzelm
parents:
33538
diff
changeset
|
281 |
((code |
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56281
diff
changeset
|
282 |
|> Runtime.debugging opt_context |
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56281
diff
changeset
|
283 |
|> 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
|
284 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
285 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
286 |
(* compiler invocation *) |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
287 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
288 |
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
|
289 |
[PolyML.Compiler.CPOutStream write, |
62941 | 290 |
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
|
291 |
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
|
292 |
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
|
293 |
PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos), |
31437 | 294 |
PolyML.Compiler.CPFileName location_props, |
62878 | 295 |
PolyML.Compiler.CPPrintDepth ML_Print_Depth.get_print_depth, |
31475 | 296 |
PolyML.Compiler.CPCompilerResultFun result_fun, |
62501 | 297 |
PolyML.Compiler.CPPrintInAlphabeticalOrder false, |
62993 | 298 |
PolyML.Compiler.CPDebug debug, |
299 |
PolyML.Compiler.CPBindingSeq serial]; |
|
60956 | 300 |
|
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
301 |
val _ = |
78759 | 302 |
Isabelle_Thread.try_catch |
303 |
(fn () => |
|
304 |
(while not (List.null (! input_buffer)) do |
|
305 |
ML_Recursive.recursive env (fn () => PolyML.compiler (get, parameters) ()))) |
|
306 |
(fn exn => |
|
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
307 |
let |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
308 |
val exn_msg = |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
309 |
(case exn of |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
310 |
STATIC_ERRORS () => "" |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
311 |
| Runtime.TOPLEVEL_ERROR => "" |
62516 | 312 |
| _ => "Exception- " ^ Pretty.string_of (Runtime.pretty_exn exn) ^ " raised"); |
78724
f2d7f4334cdc
clarified output vs. error: presence of error messages means error (see also cb7264721c91);
wenzelm
parents:
78021
diff
changeset
|
313 |
val _ = err exn_msg; |
78759 | 314 |
in expose_error true end); |
78724
f2d7f4334cdc
clarified output vs. error: presence of error messages means error (see also cb7264721c91);
wenzelm
parents:
78021
diff
changeset
|
315 |
in expose_error (#verbose flags) end; |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
316 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
317 |
end; |