author | wenzelm |
Mon, 10 Jan 2011 22:03:24 +0100 | |
changeset 41503 | a7462e442e35 |
parent 41501 | b5ad6b0d6d7c |
child 41504 | f0f20a5b54df |
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 |
|
41503
a7462e442e35
refined report_parse_tree: reverse reports happen to produce proper type information for inlined @{term}, @{typ} etc.;
wenzelm
parents:
41501
diff
changeset
|
25 |
fun offset_position_of (loc: PolyML.location) = |
a7462e442e35
refined report_parse_tree: reverse reports happen to produce proper type information for inlined @{term}, @{typ} etc.;
wenzelm
parents:
41501
diff
changeset
|
26 |
if #startPosition loc > 0 then position_of loc |
a7462e442e35
refined report_parse_tree: reverse reports happen to produce proper type information for inlined @{term}, @{typ} etc.;
wenzelm
parents:
41501
diff
changeset
|
27 |
else Position.none; |
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
|
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) ""); |
41503
a7462e442e35
refined report_parse_tree: reverse reports happen to produce proper type information for inlined @{term}, @{typ} etc.;
wenzelm
parents:
41501
diff
changeset
|
50 |
|
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
51 |
fun report loc (PolyML.PTtype types) = |
41503
a7462e442e35
refined report_parse_tree: reverse reports happen to produce proper type information for inlined @{term}, @{typ} etc.;
wenzelm
parents:
41501
diff
changeset
|
52 |
cons (fn () => |
a7462e442e35
refined report_parse_tree: reverse reports happen to produce proper type information for inlined @{term}, @{typ} etc.;
wenzelm
parents:
41501
diff
changeset
|
53 |
PolyML.NameSpace.displayTypeExpression (types, depth, space) |
a7462e442e35
refined report_parse_tree: reverse reports happen to produce proper type information for inlined @{term}, @{typ} etc.;
wenzelm
parents:
41501
diff
changeset
|
54 |
|> pretty_ml |> Pretty.from_ML |> Pretty.string_of |
a7462e442e35
refined report_parse_tree: reverse reports happen to produce proper type information for inlined @{term}, @{typ} etc.;
wenzelm
parents:
41501
diff
changeset
|
55 |
|> report_text (offset_position_of loc) Markup.ML_typing) |
a7462e442e35
refined report_parse_tree: reverse reports happen to produce proper type information for inlined @{term}, @{typ} etc.;
wenzelm
parents:
41501
diff
changeset
|
56 |
| report loc (PolyML.PTdeclaredAt decl) = cons (fn () => report_decl Markup.ML_def loc decl) |
a7462e442e35
refined report_parse_tree: reverse reports happen to produce proper type information for inlined @{term}, @{typ} etc.;
wenzelm
parents:
41501
diff
changeset
|
57 |
| report loc (PolyML.PTopenedAt decl) = cons (fn () => report_decl Markup.ML_open loc decl) |
a7462e442e35
refined report_parse_tree: reverse reports happen to produce proper type information for inlined @{term}, @{typ} etc.;
wenzelm
parents:
41501
diff
changeset
|
58 |
| report loc (PolyML.PTstructureAt decl) = |
a7462e442e35
refined report_parse_tree: reverse reports happen to produce proper type information for inlined @{term}, @{typ} etc.;
wenzelm
parents:
41501
diff
changeset
|
59 |
cons (fn () => 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
|
60 |
| 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
|
61 |
| report _ (PolyML.PTfirstChild tree) = report_tree (tree ()) |
41503
a7462e442e35
refined report_parse_tree: reverse reports happen to produce proper type information for inlined @{term}, @{typ} etc.;
wenzelm
parents:
41501
diff
changeset
|
62 |
| report _ _ = I |
a7462e442e35
refined report_parse_tree: reverse reports happen to produce proper type information for inlined @{term}, @{typ} etc.;
wenzelm
parents:
41501
diff
changeset
|
63 |
and report_tree (loc, props) = fold (report loc) props; |
a7462e442e35
refined report_parse_tree: reverse reports happen to produce proper type information for inlined @{term}, @{typ} etc.;
wenzelm
parents:
41501
diff
changeset
|
64 |
in fn tree => List.app (fn e => e ()) (report_tree tree []) end; |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
65 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
66 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
67 |
(* 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
|
68 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
69 |
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
|
70 |
let |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
71 |
val _ = Secure.secure_mltext (); |
39227 | 72 |
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
|
73 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
74 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
75 |
(* input *) |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
76 |
|
31437 | 77 |
val location_props = |
32492
9d49a280f3f9
eval/location_props: always produce YXML markup, independent of print_mode;
wenzelm
parents:
32490
diff
changeset
|
78 |
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
|
79 |
(filter (member (op =) [Markup.idN, Markup.fileN] o #1) (Position.properties_of pos)))); |
31437 | 80 |
|
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
|
81 |
val input_buffer = |
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
|
82 |
Unsynchronized.ref (toks |> map |
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
|
83 |
(`(maps (String.explode o Symbol.esc) o Symbol.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
|
84 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
85 |
fun get () = |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
86 |
(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
|
87 |
(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
|
88 |
| ([], _) :: 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
|
89 |
| [] => 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
|
90 |
|
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
|
91 |
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
|
92 |
(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
|
93 |
(_ :: _, 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
|
94 |
| ([], 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
|
95 |
| [] => 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
|
96 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
97 |
|
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
|
98 |
(* 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
|
99 |
|
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
|
100 |
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
|
101 |
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
|
102 |
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
|
103 |
|
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 |
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
|
105 |
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
|
106 |
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
|
107 |
|
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 |
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
|
109 |
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
|
110 |
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
|
111 |
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
|
112 |
|
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
|
113 |
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
|
114 |
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
|
115 |
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
|
116 |
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
|
117 |
((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
|
118 |
Pretty.string_of (Pretty.from_ML (pretty_ml msg)) ^ |
39507
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39440
diff
changeset
|
119 |
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
|
120 |
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
|
121 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
122 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
123 |
(* results *) |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
124 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
125 |
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
|
126 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
127 |
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
|
128 |
let |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
129 |
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
|
130 |
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
|
131 |
(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
|
132 |
else (); |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
133 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
134 |
fun apply_fix (a, b) = |
40799
d44c87988a24
ML results: enter before printing (cf. Poly/ML SVN 1218);
wenzelm
parents:
39507
diff
changeset
|
135 |
(#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
|
136 |
fun apply_type (a, b) = |
40799
d44c87988a24
ML results: enter before printing (cf. Poly/ML SVN 1218);
wenzelm
parents:
39507
diff
changeset
|
137 |
(#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
|
138 |
fun apply_sig (a, b) = |
40799
d44c87988a24
ML results: enter before printing (cf. Poly/ML SVN 1218);
wenzelm
parents:
39507
diff
changeset
|
139 |
(#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
|
140 |
fun apply_struct (a, b) = |
40799
d44c87988a24
ML results: enter before printing (cf. Poly/ML SVN 1218);
wenzelm
parents:
39507
diff
changeset
|
141 |
(#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
|
142 |
fun apply_funct (a, b) = |
40799
d44c87988a24
ML results: enter before printing (cf. Poly/ML SVN 1218);
wenzelm
parents:
39507
diff
changeset
|
143 |
(#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
|
144 |
fun apply_val (a, b) = |
40799
d44c87988a24
ML results: enter before printing (cf. Poly/ML SVN 1218);
wenzelm
parents:
39507
diff
changeset
|
145 |
(#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
|
146 |
in |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
147 |
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
|
148 |
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
|
149 |
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
|
150 |
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
|
151 |
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
|
152 |
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
|
153 |
end; |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
154 |
|
39231
25c345302a17
avoid mixing of static and runtime errors in compiler output, to accomodate Proof General;
wenzelm
parents:
39230
diff
changeset
|
155 |
exception STATIC_ERRORS of unit; |
39230
184507f6e8d0
ML_Compiler.eval: discontinued extra "Static Errors" of raw Poly/ML;
wenzelm
parents:
39228
diff
changeset
|
156 |
|
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
157 |
fun result_fun (phase1, phase2) () = |
31477 | 158 |
((case phase1 of |
159 |
NONE => () |
|
160 |
| SOME parse_tree => report_parse_tree depth space parse_tree); |
|
161 |
(case phase2 of |
|
39231
25c345302a17
avoid mixing of static and runtime errors in compiler output, to accomodate Proof General;
wenzelm
parents:
39230
diff
changeset
|
162 |
NONE => raise STATIC_ERRORS () |
31477 | 163 |
| SOME code => |
33603
3713a5208671
generalized Runtime.toplevel_error wrt. output function;
wenzelm
parents:
33538
diff
changeset
|
164 |
apply_result |
3713a5208671
generalized Runtime.toplevel_error wrt. output function;
wenzelm
parents:
33538
diff
changeset
|
165 |
((code |
3713a5208671
generalized Runtime.toplevel_error wrt. output function;
wenzelm
parents:
33538
diff
changeset
|
166 |
|> Runtime.debugging |
39231
25c345302a17
avoid mixing of static and runtime errors in compiler output, to accomodate Proof General;
wenzelm
parents:
39230
diff
changeset
|
167 |
|> 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
|
168 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
169 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
170 |
(* compiler invocation *) |
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 |
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
|
173 |
[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
|
174 |
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
|
175 |
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
|
176 |
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
|
177 |
PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos), |
31437 | 178 |
PolyML.Compiler.CPFileName location_props, |
31475 | 179 |
PolyML.Compiler.CPCompilerResultFun result_fun, |
180 |
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
|
181 |
val _ = |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
182 |
(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
|
183 |
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
|
184 |
handle exn => |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
185 |
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
|
186 |
else |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
187 |
let |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
188 |
val exn_msg = |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
189 |
(case exn of |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
190 |
STATIC_ERRORS () => "" |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
191 |
| Runtime.TOPLEVEL_ERROR => "" |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
192 |
| _ => "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
|
193 |
val _ = output_warnings (); |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
194 |
val _ = output_writeln (); |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39231
diff
changeset
|
195 |
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
|
196 |
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
|
197 |
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
|
198 |
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
|
199 |
end; |
31333
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
200 |
|
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
201 |
end; |
fcd010617e6c
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm
parents:
diff
changeset
|
202 |