author | wenzelm |
Sun, 09 Jan 2011 20:30:47 +0100 | |
changeset 41484 | 51310e1ccd6f |
parent 41483 | 4a8431c73cf2 |
child 41501 | b5ad6b0d6d7c |
permissions | -rw-r--r-- |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/ML/ml_compiler_polyml-5.3.ML |
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 |
|
33538
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
32738
diff
changeset
|
4 |
Advanced runtime compilation for Poly/ML 5.3.0. |
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 |
|
31429
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
10 |
(* source locations *) |
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
11 |
|
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
12 |
fun position_of (loc: PolyML.location) = |
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
13 |
let |
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
14 |
val {file = text, startLine = line, startPosition = offset, |
41483 | 15 |
endLine = _, endPosition = end_offset} = loc; |
41484 | 16 |
val props = |
31434
1f9b6a5dc8cc
more robust treatment of bootstrap source positions;
wenzelm
parents:
31429
diff
changeset
|
17 |
(case YXML.parse text of |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
37209
diff
changeset
|
18 |
XML.Elem ((e, atts), _) => if e = Markup.positionN then atts else [] |
31434
1f9b6a5dc8cc
more robust treatment of bootstrap source positions;
wenzelm
parents:
31429
diff
changeset
|
19 |
| XML.Text s => Position.file_name s); |
31429
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
20 |
in |
41484 | 21 |
Position.make |
22 |
{line = line, column = 0, offset = offset, end_offset = end_offset, props = props} |
|
23 |
end; |
|
31429
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
24 |
|
39240
a0c0698e56c0
ML_Compiler.eval: reported positions need to contain offset, to avoid displaced reports due to synthesized line numbers;
wenzelm
parents:
39232
diff
changeset
|
25 |
fun offset_position_of loc = |
a0c0698e56c0
ML_Compiler.eval: reported positions need to contain offset, to avoid displaced reports due to synthesized line numbers;
wenzelm
parents:
39232
diff
changeset
|
26 |
let val pos = position_of loc |
a0c0698e56c0
ML_Compiler.eval: reported positions need to contain offset, to avoid displaced reports due to synthesized line numbers;
wenzelm
parents:
39232
diff
changeset
|
27 |
in if is_some (Position.offset_of pos) then pos else Position.none end; |
a0c0698e56c0
ML_Compiler.eval: reported positions need to contain offset, to avoid displaced reports due to synthesized line numbers;
wenzelm
parents:
39232
diff
changeset
|
28 |
|
31477 | 29 |
fun exn_position exn = |
31429
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
30 |
(case PolyML.exceptionLocation exn of |
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
31 |
NONE => Position.none |
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
32 |
| SOME loc => position_of loc); |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
33 |
|
38874
4a4d34d2f97b
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents:
38720
diff
changeset
|
34 |
val exn_messages = Runtime.exn_messages exn_position; |
31477 | 35 |
val exn_message = Runtime.exn_message exn_position; |
36 |
||
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
37 |
|
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 |
|
31429
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
40 |
fun report_parse_tree 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
|
41 |
let |
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
|
42 |
val report_text = |
7f8bc335e203
ML_Context.eval: produce antiquotation environment preferably in invisible context, to avoid displaced report messages from ML_Compiler;
wenzelm
parents:
38228
diff
changeset
|
43 |
(case Context.thread_data () of |
7f8bc335e203
ML_Context.eval: produce antiquotation environment preferably in invisible context, to avoid displaced report messages from ML_Compiler;
wenzelm
parents:
38228
diff
changeset
|
44 |
SOME (Context.Proof ctxt) => Context_Position.report_text ctxt |
7f8bc335e203
ML_Context.eval: produce antiquotation environment preferably in invisible context, to avoid displaced report messages from ML_Compiler;
wenzelm
parents:
38228
diff
changeset
|
45 |
| _ => Position.report_text); |
7f8bc335e203
ML_Context.eval: produce antiquotation environment preferably in invisible context, to avoid displaced report messages from ML_Compiler;
wenzelm
parents:
38228
diff
changeset
|
46 |
|
31475 | 47 |
fun report_decl markup loc decl = |
39507
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39440
diff
changeset
|
48 |
report_text (offset_position_of loc) Markup.ML_ref |
39440
4c2547af5909
simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents:
39439
diff
changeset
|
49 |
(Markup.markup (Position.markup (position_of decl) markup) ""); |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
50 |
fun report loc (PolyML.PTtype types) = |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
51 |
PolyML.NameSpace.displayTypeExpression (types, depth, space) |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
52 |
|> pretty_ml |> Pretty.from_ML |> Pretty.string_of |
39507
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39440
diff
changeset
|
53 |
|> report_text (offset_position_of loc) Markup.ML_typing |
31475 | 54 |
| report loc (PolyML.PTdeclaredAt decl) = report_decl Markup.ML_def loc decl |
55 |
| report loc (PolyML.PTopenedAt decl) = report_decl Markup.ML_open loc decl |
|
56 |
| report loc (PolyML.PTstructureAt decl) = report_decl Markup.ML_struct loc decl |
|
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
57 |
| report _ (PolyML.PTnextSibling tree) = report_tree (tree ()) |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
58 |
| report _ (PolyML.PTfirstChild tree) = report_tree (tree ()) |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
59 |
| report _ _ = () |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
60 |
and report_tree (loc, props) = List.app (report loc) props; |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
61 |
in report_tree end; |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
62 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
63 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
64 |
(* 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
|
65 |
|
31756
178621145f98
eval: tuned input buffer and get_offset (which ran very hot, up to the point where AFP/FlyspeckTame would seemingly take forever);
wenzelm
parents:
31495
diff
changeset
|
66 |
val offset_of = the_default 0 o Position.offset_of; |
178621145f98
eval: tuned input buffer and get_offset (which ran very hot, up to the point where AFP/FlyspeckTame would seemingly take forever);
wenzelm
parents:
31495
diff
changeset
|
67 |
|
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
68 |
fun eval verbose pos toks = |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
69 |
let |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
70 |
val _ = Secure.secure_mltext (); |
39227 | 71 |
val space = ML_Env.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
|
72 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
73 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
74 |
(* input *) |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
75 |
|
31437 | 76 |
val location_props = |
32492
9d49a280f3f9
eval/location_props: always produce YXML markup, independent of print_mode;
wenzelm
parents:
32490
diff
changeset
|
77 |
op ^ (YXML.output_markup (Markup.position |> Markup.properties |
9d49a280f3f9
eval/location_props: always produce YXML markup, independent of print_mode;
wenzelm
parents:
32490
diff
changeset
|
78 |
(filter (member (op =) [Markup.idN, Markup.fileN] o #1) (Position.properties_of pos)))); |
31437 | 79 |
|
31429
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
80 |
val input = toks |> maps (fn tok => |
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
81 |
let |
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
82 |
val syms = Symbol.explode (ML_Lex.check_content_of tok); |
31437 | 83 |
val (ps, _) = fold_map (fn s => fn p => (p, Position.advance s p)) syms |
84 |
(Position.reset_range (ML_Lex.pos_of tok)); |
|
31756
178621145f98
eval: tuned input buffer and get_offset (which ran very hot, up to the point where AFP/FlyspeckTame would seemingly take forever);
wenzelm
parents:
31495
diff
changeset
|
85 |
in |
178621145f98
eval: tuned input buffer and get_offset (which ran very hot, up to the point where AFP/FlyspeckTame would seemingly take forever);
wenzelm
parents:
31495
diff
changeset
|
86 |
(ps ~~ syms) |> maps (fn (p, sym) => |
178621145f98
eval: tuned input buffer and get_offset (which ran very hot, up to the point where AFP/FlyspeckTame would seemingly take forever);
wenzelm
parents:
31495
diff
changeset
|
87 |
map (pair (offset_of p)) (String.explode (Symbol.esc sym))) |
178621145f98
eval: tuned input buffer and get_offset (which ran very hot, up to the point where AFP/FlyspeckTame would seemingly take forever);
wenzelm
parents:
31495
diff
changeset
|
88 |
end); |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
89 |
|
37209
1c8cf0048934
terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents:
33603
diff
changeset
|
90 |
val input_buffer = Unsynchronized.ref input; |
32738 | 91 |
val line = Unsynchronized.ref (the_default 1 (Position.line_of pos)); |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
92 |
|
31756
178621145f98
eval: tuned input buffer and get_offset (which ran very hot, up to the point where AFP/FlyspeckTame would seemingly take forever);
wenzelm
parents:
31495
diff
changeset
|
93 |
fun get_offset () = (case ! input_buffer of [] => 0 | (i, _) :: _ => i); |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
94 |
fun get () = |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
95 |
(case ! input_buffer of |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
96 |
[] => NONE |
31756
178621145f98
eval: tuned input buffer and get_offset (which ran very hot, up to the point where AFP/FlyspeckTame would seemingly take forever);
wenzelm
parents:
31495
diff
changeset
|
97 |
| (_, c) :: rest => |
178621145f98
eval: tuned input buffer and get_offset (which ran very hot, up to the point where AFP/FlyspeckTame would seemingly take forever);
wenzelm
parents:
31495
diff
changeset
|
98 |
(input_buffer := rest; |
31429
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
99 |
if c = #"\n" then line := ! line + 1 else (); |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
100 |
SOME c)); |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
101 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
102 |
|
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
|
103 |
(* output channels *) |
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
|
104 |
|
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
|
105 |
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
|
106 |
fun write s = Unsynchronized.change writeln_buffer (Buffer.add s); |
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
|
107 |
fun output_writeln () = writeln (Buffer.content (! writeln_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
|
108 |
|
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
|
109 |
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
|
110 |
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
|
111 |
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
|
112 |
|
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
|
113 |
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
|
114 |
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
|
115 |
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
|
116 |
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
|
117 |
|
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
|
118 |
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
|
119 |
let |
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
|
120 |
val txt = |
39439
1c294d150ded
eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents:
39240
diff
changeset
|
121 |
Markup.markup Markup.no_report |
39240
a0c0698e56c0
ML_Compiler.eval: reported positions need to contain offset, to avoid displaced reports due to synthesized line numbers;
wenzelm
parents:
39232
diff
changeset
|
122 |
((if hard then "Error" else "Warning") ^ Position.str_of (position_of loc) ^ ":\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
|
123 |
Pretty.string_of (Pretty.from_ML (pretty_ml msg)) ^ |
39507
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39440
diff
changeset
|
124 |
Position.reported_text (offset_position_of loc) Markup.report ""; |
39231
25c345302a17
avoid mixing of static and runtime errors in compiler output, to accomodate Proof General;
wenzelm
parents:
39230
diff
changeset
|
125 |
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
|
126 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
127 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
128 |
(* results *) |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
129 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
130 |
val depth = get_print_depth (); |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
131 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
132 |
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
|
133 |
let |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
134 |
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
|
135 |
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
|
136 |
(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
|
137 |
else (); |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
138 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
139 |
fun apply_fix (a, b) = |
40799
d44c87988a24
ML results: enter before printing (cf. Poly/ML SVN 1218);
wenzelm
parents:
39507
diff
changeset
|
140 |
(#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
|
141 |
fun apply_type (a, b) = |
40799
d44c87988a24
ML results: enter before printing (cf. Poly/ML SVN 1218);
wenzelm
parents:
39507
diff
changeset
|
142 |
(#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
|
143 |
fun apply_sig (a, b) = |
40799
d44c87988a24
ML results: enter before printing (cf. Poly/ML SVN 1218);
wenzelm
parents:
39507
diff
changeset
|
144 |
(#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
|
145 |
fun apply_struct (a, b) = |
40799
d44c87988a24
ML results: enter before printing (cf. Poly/ML SVN 1218);
wenzelm
parents:
39507
diff
changeset
|
146 |
(#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
|
147 |
fun apply_funct (a, b) = |
40799
d44c87988a24
ML results: enter before printing (cf. Poly/ML SVN 1218);
wenzelm
parents:
39507
diff
changeset
|
148 |
(#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
|
149 |
fun apply_val (a, b) = |
40799
d44c87988a24
ML results: enter before printing (cf. Poly/ML SVN 1218);
wenzelm
parents:
39507
diff
changeset
|
150 |
(#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
|
151 |
in |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
152 |
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
|
153 |
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
|
154 |
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
|
155 |
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
|
156 |
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
|
157 |
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
|
158 |
end; |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
159 |
|
39231
25c345302a17
avoid mixing of static and runtime errors in compiler output, to accomodate Proof General;
wenzelm
parents:
39230
diff
changeset
|
160 |
exception STATIC_ERRORS of unit; |
39230
184507f6e8d0
ML_Compiler.eval: discontinued extra "Static Errors" of raw Poly/ML;
wenzelm
parents:
39228
diff
changeset
|
161 |
|
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
162 |
fun result_fun (phase1, phase2) () = |
31477 | 163 |
((case phase1 of |
164 |
NONE => () |
|
165 |
| SOME parse_tree => report_parse_tree depth space parse_tree); |
|
166 |
(case phase2 of |
|
39231
25c345302a17
avoid mixing of static and runtime errors in compiler output, to accomodate Proof General;
wenzelm
parents:
39230
diff
changeset
|
167 |
NONE => raise STATIC_ERRORS () |
31477 | 168 |
| SOME code => |
33603
3713a5208671
generalized Runtime.toplevel_error wrt. output function;
wenzelm
parents:
33538
diff
changeset
|
169 |
apply_result |
3713a5208671
generalized Runtime.toplevel_error wrt. output function;
wenzelm
parents:
33538
diff
changeset
|
170 |
((code |
3713a5208671
generalized Runtime.toplevel_error wrt. output function;
wenzelm
parents:
33538
diff
changeset
|
171 |
|> Runtime.debugging |
39231
25c345302a17
avoid mixing of static and runtime errors in compiler output, to accomodate Proof General;
wenzelm
parents:
39230
diff
changeset
|
172 |
|> Runtime.toplevel_error (err o 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
|
173 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
174 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
175 |
(* compiler invocation *) |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
176 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
177 |
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
|
178 |
[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
|
179 |
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
|
180 |
PolyML.Compiler.CPErrorMessageProc message, |
31429
8a7c0899e0b1
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm
parents:
31333
diff
changeset
|
181 |
PolyML.Compiler.CPLineNo (fn () => ! line), |
31475 | 182 |
PolyML.Compiler.CPLineOffset get_offset, |
31437 | 183 |
PolyML.Compiler.CPFileName location_props, |
31475 | 184 |
PolyML.Compiler.CPCompilerResultFun result_fun, |
185 |
PolyML.Compiler.CPPrintInAlphabeticalOrder false]; |
|
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
186 |
val _ = |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
187 |
(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
|
188 |
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
|
189 |
handle exn => |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
190 |
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
|
191 |
else |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
192 |
let |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
193 |
val exn_msg = |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
194 |
(case exn of |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
195 |
STATIC_ERRORS () => "" |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
196 |
| Runtime.TOPLEVEL_ERROR => "" |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
197 |
| _ => "Exception- " ^ General.exnMessage exn ^ " raised"); |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
198 |
val _ = output_warnings (); |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
199 |
val _ = output_writeln (); |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
200 |
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
|
201 |
in |
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
|
202 |
if verbose then (output_warnings (); flush_error (); output_writeln ()) |
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
|
203 |
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
|
204 |
end; |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
205 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
206 |
end; |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
207 |