wenzelm@33540
|
1 |
(* Title: Pure/ML-Systems/polyml.ML
|
wenzelm@29714
|
2 |
|
wenzelm@33540
|
3 |
Compatibility wrapper for Poly/ML 5.3.0.
|
wenzelm@29714
|
4 |
*)
|
wenzelm@29714
|
5 |
|
wenzelm@32776
|
6 |
use "ML-Systems/unsynchronized.ML";
|
wenzelm@32776
|
7 |
|
wenzelm@29714
|
8 |
open Thread;
|
wenzelm@30688
|
9 |
|
wenzelm@30688
|
10 |
structure ML_Name_Space =
|
wenzelm@30688
|
11 |
struct
|
wenzelm@30688
|
12 |
open PolyML.NameSpace;
|
wenzelm@30688
|
13 |
type T = PolyML.NameSpace.nameSpace;
|
wenzelm@30688
|
14 |
val global = PolyML.globalNameSpace;
|
wenzelm@30688
|
15 |
end;
|
wenzelm@30688
|
16 |
|
wenzelm@31431
|
17 |
fun reraise exn =
|
wenzelm@31431
|
18 |
(case PolyML.exceptionLocation exn of
|
wenzelm@31431
|
19 |
NONE => raise exn
|
wenzelm@31431
|
20 |
| SOME location => PolyML.raiseWithLocation (exn, location));
|
wenzelm@31431
|
21 |
|
wenzelm@29714
|
22 |
use "ML-Systems/polyml_common.ML";
|
wenzelm@29714
|
23 |
use "ML-Systems/multithreading_polyml.ML";
|
wenzelm@29714
|
24 |
|
wenzelm@29714
|
25 |
val pointer_eq = PolyML.pointerEq;
|
wenzelm@29714
|
26 |
|
wenzelm@29714
|
27 |
fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
|
wenzelm@29714
|
28 |
|
wenzelm@31312
|
29 |
use "ML-Systems/compiler_polyml-5.3.ML";
|
wenzelm@32778
|
30 |
PolyML.Compiler.reportUnreferencedIds := true;
|
wenzelm@30629
|
31 |
|
wenzelm@30629
|
32 |
|
wenzelm@30629
|
33 |
(* toplevel pretty printing *)
|
wenzelm@30629
|
34 |
|
wenzelm@30691
|
35 |
val pretty_ml =
|
wenzelm@30691
|
36 |
let
|
wenzelm@31318
|
37 |
fun convert len (PolyML.PrettyBlock (ind, _, context, prts)) =
|
wenzelm@30691
|
38 |
let
|
wenzelm@30691
|
39 |
fun property name default =
|
wenzelm@31318
|
40 |
(case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of
|
wenzelm@31318
|
41 |
SOME (PolyML.ContextProperty (_, b)) => b
|
wenzelm@30691
|
42 |
| NONE => default);
|
wenzelm@30691
|
43 |
val bg = property "begin" "";
|
wenzelm@30691
|
44 |
val en = property "end" "";
|
wenzelm@30691
|
45 |
val len' = property "length" len;
|
wenzelm@30691
|
46 |
in ML_Pretty.Block ((bg, en), map (convert len') prts, ind) end
|
wenzelm@31318
|
47 |
| convert len (PolyML.PrettyString s) =
|
wenzelm@30691
|
48 |
ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s)
|
wenzelm@31318
|
49 |
| convert _ (PolyML.PrettyBreak (wd, _)) =
|
wenzelm@30691
|
50 |
ML_Pretty.Break (if wd < 99999 then (false, wd) else (true, 2));
|
wenzelm@30691
|
51 |
in convert "" end;
|
wenzelm@30642
|
52 |
|
wenzelm@30691
|
53 |
fun ml_pretty (ML_Pretty.Block ((bg, en), prts, ind)) =
|
wenzelm@30694
|
54 |
let val context =
|
wenzelm@31318
|
55 |
(if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @
|
wenzelm@31318
|
56 |
(if en = "" then [] else [PolyML.ContextProperty ("end", en)])
|
wenzelm@31318
|
57 |
in PolyML.PrettyBlock (ind, false, context, map ml_pretty prts) end
|
wenzelm@30691
|
58 |
| ml_pretty (ML_Pretty.String (s, len)) =
|
wenzelm@31318
|
59 |
if len = size s then PolyML.PrettyString s
|
wenzelm@31318
|
60 |
else PolyML.PrettyBlock
|
wenzelm@31318
|
61 |
(0, false, [PolyML.ContextProperty ("length", Int.toString len)], [PolyML.PrettyString s])
|
wenzelm@31318
|
62 |
| ml_pretty (ML_Pretty.Break (false, wd)) = PolyML.PrettyBreak (wd, 0)
|
wenzelm@31318
|
63 |
| ml_pretty (ML_Pretty.Break (true, _)) = PolyML.PrettyBreak (99999, 0);
|
wenzelm@30629
|
64 |
|
wenzelm@30688
|
65 |
fun toplevel_pp context (_: string list) pp =
|
wenzelm@30688
|
66 |
use_text context (1, "pp") false
|
wenzelm@31318
|
67 |
("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
|
wenzelm@30629
|
68 |
|