author | wenzelm |
Wed, 07 Sep 2011 20:49:45 +0200 | |
changeset 44801 | a0459c50cfc9 |
parent 44249 | 64620f1d6f87 |
child 47980 | c81801f881b3 |
permissions | -rw-r--r-- |
33538
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
32778
diff
changeset
|
1 |
(* Title: Pure/ML-Systems/polyml.ML |
29714
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
2 |
|
38470
484e483eb606
discontinued support for Poly/ML 5.0 and 5.1 versions;
wenzelm
parents:
36162
diff
changeset
|
3 |
Compatibility wrapper for Poly/ML 5.3 and 5.4. |
29714
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
4 |
*) |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
5 |
|
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
6 |
open Thread; |
30673 | 7 |
|
8 |
structure ML_Name_Space = |
|
9 |
struct |
|
10 |
open PolyML.NameSpace; |
|
11 |
type T = PolyML.NameSpace.nameSpace; |
|
12 |
val global = PolyML.globalNameSpace; |
|
13 |
end; |
|
14 |
||
31427
5a07cc86675d
reraise exceptions to preserve original position (ML system specific);
wenzelm
parents:
31318
diff
changeset
|
15 |
fun reraise exn = |
5a07cc86675d
reraise exceptions to preserve original position (ML system specific);
wenzelm
parents:
31318
diff
changeset
|
16 |
(case PolyML.exceptionLocation exn of |
5a07cc86675d
reraise exceptions to preserve original position (ML system specific);
wenzelm
parents:
31318
diff
changeset
|
17 |
NONE => raise exn |
5a07cc86675d
reraise exceptions to preserve original position (ML system specific);
wenzelm
parents:
31318
diff
changeset
|
18 |
| SOME location => PolyML.raiseWithLocation (exn, location)); |
5a07cc86675d
reraise exceptions to preserve original position (ML system specific);
wenzelm
parents:
31318
diff
changeset
|
19 |
|
44249
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
43948
diff
changeset
|
20 |
fun set_exn_serial i exn = |
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
43948
diff
changeset
|
21 |
let |
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
43948
diff
changeset
|
22 |
val (file, startLine, endLine) = |
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
43948
diff
changeset
|
23 |
(case PolyML.exceptionLocation exn of |
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
43948
diff
changeset
|
24 |
NONE => ("", 0, 0) |
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
43948
diff
changeset
|
25 |
| SOME {file, startLine, endLine, startPosition, ...} => (file, startLine, endLine)); |
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
43948
diff
changeset
|
26 |
val location = |
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
43948
diff
changeset
|
27 |
{file = file, startLine = startLine, endLine = endLine, |
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
43948
diff
changeset
|
28 |
startPosition = ~ i, endPosition = 0}; |
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
43948
diff
changeset
|
29 |
in PolyML.raiseWithLocation (exn, location) handle e => e end; |
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
43948
diff
changeset
|
30 |
|
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
43948
diff
changeset
|
31 |
fun get_exn_serial exn = |
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
43948
diff
changeset
|
32 |
(case Option.map #startPosition (PolyML.exceptionLocation exn) of |
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
43948
diff
changeset
|
33 |
NONE => NONE |
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
43948
diff
changeset
|
34 |
| SOME i => if i >= 0 then NONE else SOME (~ i)); |
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
43948
diff
changeset
|
35 |
|
29714
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
36 |
use "ML-Systems/polyml_common.ML"; |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
37 |
use "ML-Systems/multithreading_polyml.ML"; |
39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
38470
diff
changeset
|
38 |
use "ML-Systems/unsynchronized.ML"; |
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
38470
diff
changeset
|
39 |
|
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
38470
diff
changeset
|
40 |
val _ = PolyML.Compiler.forgetValue "ref"; |
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
38470
diff
changeset
|
41 |
val _ = PolyML.Compiler.forgetType "ref"; |
29714
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
42 |
|
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
43 |
val pointer_eq = PolyML.pointerEq; |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
44 |
|
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
45 |
fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction; |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
46 |
|
31312 | 47 |
use "ML-Systems/compiler_polyml-5.3.ML"; |
32778 | 48 |
PolyML.Compiler.reportUnreferencedIds := true; |
30626 | 49 |
|
50 |
||
51 |
(* toplevel pretty printing *) |
|
52 |
||
30676
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset
|
53 |
val pretty_ml = |
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset
|
54 |
let |
31318 | 55 |
fun convert len (PolyML.PrettyBlock (ind, _, context, prts)) = |
30676
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset
|
56 |
let |
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset
|
57 |
fun property name default = |
31318 | 58 |
(case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of |
59 |
SOME (PolyML.ContextProperty (_, b)) => b |
|
30676
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset
|
60 |
| NONE => default); |
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset
|
61 |
val bg = property "begin" ""; |
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset
|
62 |
val en = property "end" ""; |
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset
|
63 |
val len' = property "length" len; |
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset
|
64 |
in ML_Pretty.Block ((bg, en), map (convert len') prts, ind) end |
31318 | 65 |
| convert len (PolyML.PrettyString s) = |
30676
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset
|
66 |
ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s) |
31318 | 67 |
| convert _ (PolyML.PrettyBreak (wd, _)) = |
30676
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset
|
68 |
ML_Pretty.Break (if wd < 99999 then (false, wd) else (true, 2)); |
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset
|
69 |
in convert "" end; |
30638 | 70 |
|
30676
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset
|
71 |
fun ml_pretty (ML_Pretty.Block ((bg, en), prts, ind)) = |
30679 | 72 |
let val context = |
31318 | 73 |
(if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @ |
74 |
(if en = "" then [] else [PolyML.ContextProperty ("end", en)]) |
|
75 |
in PolyML.PrettyBlock (ind, false, context, map ml_pretty prts) end |
|
30676
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset
|
76 |
| ml_pretty (ML_Pretty.String (s, len)) = |
31318 | 77 |
if len = size s then PolyML.PrettyString s |
78 |
else PolyML.PrettyBlock |
|
79 |
(0, false, [PolyML.ContextProperty ("length", Int.toString len)], [PolyML.PrettyString s]) |
|
80 |
| ml_pretty (ML_Pretty.Break (false, wd)) = PolyML.PrettyBreak (wd, 0) |
|
81 |
| ml_pretty (ML_Pretty.Break (true, _)) = PolyML.PrettyBreak (99999, 0); |
|
30626 | 82 |
|
30673 | 83 |
fun toplevel_pp context (_: string list) pp = |
84 |
use_text context (1, "pp") false |
|
31318 | 85 |
("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))"); |
30626 | 86 |
|
36162
0bd034a80a9a
added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;
wenzelm
parents:
33543
diff
changeset
|
87 |
val ml_make_string = |
0bd034a80a9a
added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;
wenzelm
parents:
33543
diff
changeset
|
88 |
"(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, get_print_depth ())))))"; |
0bd034a80a9a
added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;
wenzelm
parents:
33543
diff
changeset
|
89 |
|
43948 | 90 |
use "ML-Systems/ml_system.ML"; |
91 |