author | wenzelm |
Fri, 17 Jul 2015 17:17:39 +0200 | |
changeset 60746 | 8cf877aca29a |
parent 60745 | d86b4cd0f1ec |
child 60858 | 7bf2188a0998 |
permissions | -rw-r--r-- |
47980
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
45666
diff
changeset
|
1 |
(* Title: Pure/ML/ml_compiler_polyml.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 |
|
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56281
diff
changeset
|
4 |
Runtime compilation and evaluation -- Poly/ML version. |
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 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
7 |
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
|
8 |
struct |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
9 |
|
56281 | 10 |
open ML_Compiler; |
11 |
||
12 |
||
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
13 |
(* parse trees *) |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
14 |
|
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
|
15 |
fun report_parse_tree redirect depth 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
|
16 |
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
|
17 |
val is_visible = |
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
|
18 |
(case Context.thread_data () 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
|
19 |
SOME context => Context_Position.is_visible_generic context |
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
|
20 |
| NONE => true); |
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
|
21 |
fun is_reported pos = is_visible andalso Position.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
|
22 |
|
60744 | 23 |
|
24 |
(* syntax reports *) |
|
25 |
||
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
|
26 |
fun reported_types loc types = |
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
|
27 |
let val pos = Exn_Properties.position_of loc in |
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
|
28 |
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
|
29 |
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
|
30 |
val xml = |
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
|
31 |
PolyML.NameSpace.displayTypeExpression (types, depth, space) |
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
|
32 |
|> pretty_ml |> Pretty.from_ML |> Pretty.string_of |
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
|
33 |
|> 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
|
34 |
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
|
35 |
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
|
36 |
|
44737 | 37 |
fun reported_entity kind loc decl = |
58991
92b6f4e68c5a
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
56618
diff
changeset
|
38 |
let |
92b6f4e68c5a
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
56618
diff
changeset
|
39 |
val pos = Exn_Properties.position_of loc; |
92b6f4e68c5a
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
56618
diff
changeset
|
40 |
val def_pos = Exn_Properties.position_of decl; |
92b6f4e68c5a
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
56618
diff
changeset
|
41 |
in |
92b6f4e68c5a
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
56618
diff
changeset
|
42 |
(is_reported pos andalso pos <> def_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
|
43 |
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
|
44 |
fun markup () = |
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
|
45 |
(Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of def_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
|
46 |
in cons (pos, markup, fn () => "") 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
|
47 |
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
|
48 |
|
60731
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
60730
diff
changeset
|
49 |
fun reported_completions loc names = |
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
60730
diff
changeset
|
50 |
let val pos = Exn_Properties.position_of loc in |
60732 | 51 |
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
|
52 |
let |
60732 | 53 |
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
|
54 |
val xml = Completion.encode completion; |
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
60730
diff
changeset
|
55 |
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
|
56 |
else I |
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
60730
diff
changeset
|
57 |
end; |
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
60730
diff
changeset
|
58 |
|
60744 | 59 |
fun reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ()) |
60 |
| reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ()) |
|
61 |
| 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
|
62 |
| reported loc (PolyML.PTdeclaredAt decl) = reported_entity Markup.ML_defN loc decl |
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 |
| reported loc (PolyML.PTopenedAt decl) = reported_entity Markup.ML_openN loc decl |
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 |
| reported loc (PolyML.PTstructureAt decl) = reported_entity Markup.ML_structureN loc decl |
60731
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
60730
diff
changeset
|
65 |
| reported loc pt = |
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
60730
diff
changeset
|
66 |
(case ML_Parse_Tree.completions pt of |
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
60730
diff
changeset
|
67 |
SOME names => reported_completions loc names |
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
60730
diff
changeset
|
68 |
| NONE => I) |
44737 | 69 |
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
|
70 |
|
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 |
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
|
72 |
|
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
|
73 |
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
|
74 |
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
|
75 |
|> 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
|
76 |
|> Output.report; |
60744 | 77 |
val _ = |
78 |
if not (null persistent_reports) andalso redirect andalso Multithreading.enabled () |
|
79 |
then |
|
80 |
Execution.print |
|
81 |
{name = "ML_Compiler.report", pos = Position.thread_data (), pri = Task_Queue.urgent_pri} |
|
82 |
output |
|
83 |
else output (); |
|
84 |
||
85 |
||
86 |
(* breakpoints *) |
|
87 |
||
88 |
fun breakpoints _ (PolyML.PTnextSibling tree) = breakpoints_tree (tree ()) |
|
89 |
| breakpoints _ (PolyML.PTfirstChild tree) = breakpoints_tree (tree ()) |
|
90 |
| breakpoints loc pt = |
|
91 |
(case ML_Parse_Tree.breakpoint pt of |
|
92 |
SOME b => |
|
93 |
let val pos = Exn_Properties.position_of loc in |
|
94 |
if is_reported pos then |
|
95 |
let val id = serial (); |
|
60746 | 96 |
in cons ((pos, Markup.ML_breakpoint id), (id, (b, pos))) end |
60744 | 97 |
else I |
98 |
end |
|
99 |
| NONE => I) |
|
100 |
and breakpoints_tree (loc, props) = fold (breakpoints loc) props; |
|
101 |
||
102 |
val all_breakpoints = rev (breakpoints_tree parse_tree []); |
|
103 |
val _ = Position.reports (map #1 all_breakpoints); |
|
60746 | 104 |
val _ = |
105 |
if is_some (Context.thread_data ()) then |
|
106 |
Context.>> (fold (ML_Env.add_breakpoint o #2) all_breakpoints) |
|
107 |
else (); |
|
108 |
in () end; |
|
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
109 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
110 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
111 |
(* 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
|
112 |
|
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 |
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
|
114 |
let |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
115 |
val _ = Secure.secure_mltext (); |
60746 | 116 |
val space = ML_Env.name_space {SML = #SML flags, exchange = #exchange flags}; |
56265
785569927666
discontinued Toplevel.debug in favour of system option "exception_trace";
wenzelm
parents:
55837
diff
changeset
|
117 |
val opt_context = Context.thread_data (); |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
118 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
119 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
120 |
(* input *) |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
121 |
|
50911
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
50910
diff
changeset
|
122 |
val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos))); |
31437 | 123 |
|
59110
8a78c7cb5b14
some special cases for official SML, to treat Isabelle symbols like raw characters;
wenzelm
parents:
58991
diff
changeset
|
124 |
val input_explode = |
8a78c7cb5b14
some special cases for official SML, to treat Isabelle symbols like raw characters;
wenzelm
parents:
58991
diff
changeset
|
125 |
if #SML flags then String.explode |
8a78c7cb5b14
some special cases for official SML, to treat Isabelle symbols like raw characters;
wenzelm
parents:
58991
diff
changeset
|
126 |
else maps (String.explode o Symbol.esc) o Symbol.explode; |
8a78c7cb5b14
some special cases for official SML, to treat Isabelle symbols like raw characters;
wenzelm
parents:
58991
diff
changeset
|
127 |
|
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
|
128 |
val input_buffer = |
59110
8a78c7cb5b14
some special cases for official SML, to treat Isabelle symbols like raw characters;
wenzelm
parents:
58991
diff
changeset
|
129 |
Unsynchronized.ref (toks |> map (`(input_explode o ML_Lex.check_content_of))); |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
130 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
131 |
fun get () = |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
132 |
(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
|
133 |
(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
|
134 |
| ([], _) :: 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
|
135 |
| [] => 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
|
136 |
|
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
|
137 |
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
|
138 |
(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
|
139 |
(_ :: _, 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
|
140 |
| ([], 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
|
141 |
| [] => 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
|
142 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
143 |
|
60744 | 144 |
(* 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
|
145 |
|
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
|
146 |
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
|
147 |
fun write s = Unsynchronized.change writeln_buffer (Buffer.add s); |
54389 | 148 |
fun output_writeln () = writeln (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
|
149 |
|
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
|
150 |
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
|
151 |
fun warn msg = Unsynchronized.change warnings (cons msg); |
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
|
152 |
fun output_warnings () = List.app warning (rev (! warnings)); |
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
|
153 |
|
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
|
154 |
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
|
155 |
fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n"); |
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
|
156 |
fun flush_error () = writeln (Buffer.content (! error_buffer)); |
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
|
157 |
fun raise_error msg = error (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
|
158 |
|
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
|
159 |
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
|
160 |
let |
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56281
diff
changeset
|
161 |
val pos = Exn_Properties.position_of 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
|
162 |
val txt = |
49828
5631ee099293
more basic ML compiler messages -- avoid conflict of 638cefe3ee99 and cb7264721c91 concerning Protocol.message_positions;
wenzelm
parents:
48992
diff
changeset
|
163 |
(if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^ |
5631ee099293
more basic ML compiler messages -- avoid conflict of 638cefe3ee99 and cb7264721c91 concerning Protocol.message_positions;
wenzelm
parents:
48992
diff
changeset
|
164 |
Pretty.string_of (Pretty.from_ML (pretty_ml msg)); |
39231
25c345302a17
avoid mixing of static and runtime errors in compiler output, to accomodate Proof General;
wenzelm
parents:
39230
diff
changeset
|
165 |
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
|
166 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
167 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
168 |
(* results *) |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
169 |
|
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56281
diff
changeset
|
170 |
val depth = ML_Options.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
|
171 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
172 |
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
|
173 |
let |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
174 |
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
|
175 |
if depth > 0 then |
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
|
176 |
(disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> write; 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
|
177 |
else (); |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
178 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
179 |
fun apply_fix (a, b) = |
40799
d44c87988a24
ML results: enter before printing (cf. Poly/ML SVN 1218);
wenzelm
parents:
39507
diff
changeset
|
180 |
(#enterFix space (a, b); display PolyML.NameSpace.displayFix (a, b)); |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
181 |
fun apply_type (a, b) = |
40799
d44c87988a24
ML results: enter before printing (cf. Poly/ML SVN 1218);
wenzelm
parents:
39507
diff
changeset
|
182 |
(#enterType space (a, b); display PolyML.NameSpace.displayType (b, depth, space)); |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
183 |
fun apply_sig (a, b) = |
40799
d44c87988a24
ML results: enter before printing (cf. Poly/ML SVN 1218);
wenzelm
parents:
39507
diff
changeset
|
184 |
(#enterSig space (a, b); display PolyML.NameSpace.displaySig (b, depth, space)); |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
185 |
fun apply_struct (a, b) = |
40799
d44c87988a24
ML results: enter before printing (cf. Poly/ML SVN 1218);
wenzelm
parents:
39507
diff
changeset
|
186 |
(#enterStruct space (a, b); display PolyML.NameSpace.displayStruct (b, depth, space)); |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
187 |
fun apply_funct (a, b) = |
40799
d44c87988a24
ML results: enter before printing (cf. Poly/ML SVN 1218);
wenzelm
parents:
39507
diff
changeset
|
188 |
(#enterFunct space (a, b); display PolyML.NameSpace.displayFunct (b, depth, space)); |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
189 |
fun apply_val (a, b) = |
40799
d44c87988a24
ML results: enter before printing (cf. Poly/ML SVN 1218);
wenzelm
parents:
39507
diff
changeset
|
190 |
(#enterVal space (a, b); display PolyML.NameSpace.displayVal (b, depth, space)); |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
191 |
in |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
192 |
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
|
193 |
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
|
194 |
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
|
195 |
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
|
196 |
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
|
197 |
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
|
198 |
end; |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
199 |
|
39231
25c345302a17
avoid mixing of static and runtime errors in compiler output, to accomodate Proof General;
wenzelm
parents:
39230
diff
changeset
|
200 |
exception STATIC_ERRORS of unit; |
39230
184507f6e8d0
ML_Compiler.eval: discontinued extra "Static Errors" of raw Poly/ML;
wenzelm
parents:
39228
diff
changeset
|
201 |
|
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
202 |
fun result_fun (phase1, phase2) () = |
31477 | 203 |
((case phase1 of |
204 |
NONE => () |
|
60746 | 205 |
| SOME parse_tree => report_parse_tree (#redirect flags) depth space parse_tree); |
31477 | 206 |
(case phase2 of |
39231
25c345302a17
avoid mixing of static and runtime errors in compiler output, to accomodate Proof General;
wenzelm
parents:
39230
diff
changeset
|
207 |
NONE => raise STATIC_ERRORS () |
31477 | 208 |
| SOME code => |
33603
3713a5208671
generalized Runtime.toplevel_error wrt. output function;
wenzelm
parents:
33538
diff
changeset
|
209 |
apply_result |
3713a5208671
generalized Runtime.toplevel_error wrt. output function;
wenzelm
parents:
33538
diff
changeset
|
210 |
((code |
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56281
diff
changeset
|
211 |
|> Runtime.debugging opt_context |
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56281
diff
changeset
|
212 |
|> 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
|
213 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
214 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
215 |
(* compiler invocation *) |
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 |
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
|
218 |
[PolyML.Compiler.CPOutStream write, |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
219 |
PolyML.Compiler.CPNameSpace 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
|
220 |
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
|
221 |
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
|
222 |
PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos), |
31437 | 223 |
PolyML.Compiler.CPFileName location_props, |
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56281
diff
changeset
|
224 |
PolyML.Compiler.CPPrintDepth ML_Options.get_print_depth, |
31475 | 225 |
PolyML.Compiler.CPCompilerResultFun result_fun, |
60730 | 226 |
PolyML.Compiler.CPPrintInAlphabeticalOrder false] @ |
60745
d86b4cd0f1ec
clarified ML compiler parameters: always provide PolyML.Compiler.CPDebug, ignore global default;
wenzelm
parents:
60744
diff
changeset
|
227 |
ML_Compiler_Parameters.debug (ML_Options.debugger_enabled opt_context); |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
228 |
val _ = |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
229 |
(while not (List.null (! input_buffer)) do |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
230 |
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
|
231 |
handle exn => |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
232 |
if Exn.is_interrupt exn then reraise exn |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
233 |
else |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
234 |
let |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
235 |
val exn_msg = |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
236 |
(case exn of |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
237 |
STATIC_ERRORS () => "" |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
238 |
| Runtime.TOPLEVEL_ERROR => "" |
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56281
diff
changeset
|
239 |
| _ => "Exception- " ^ Pretty.string_of (Exn_Output.pretty exn) ^ " raised"); |
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
240 |
val _ = output_warnings (); |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
241 |
val _ = output_writeln (); |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
242 |
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
|
243 |
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
|
244 |
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
|
245 |
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
|
246 |
end; |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
247 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
248 |
end; |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
249 |