wenzelm@29714
|
1 |
(* Title: Pure/ML-Systems/polyml.ML
|
wenzelm@29714
|
2 |
|
wenzelm@29714
|
3 |
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
|
wenzelm@29714
|
4 |
*)
|
wenzelm@29714
|
5 |
|
wenzelm@29714
|
6 |
open Thread;
|
wenzelm@30688
|
7 |
|
wenzelm@30688
|
8 |
structure ML_Name_Space =
|
wenzelm@30688
|
9 |
struct
|
wenzelm@30688
|
10 |
open PolyML.NameSpace;
|
wenzelm@30688
|
11 |
type T = PolyML.NameSpace.nameSpace;
|
wenzelm@30688
|
12 |
val global = PolyML.globalNameSpace;
|
wenzelm@30688
|
13 |
end;
|
wenzelm@30688
|
14 |
|
wenzelm@29714
|
15 |
use "ML-Systems/polyml_common.ML";
|
wenzelm@29714
|
16 |
use "ML-Systems/multithreading_polyml.ML";
|
wenzelm@29714
|
17 |
|
wenzelm@29714
|
18 |
val pointer_eq = PolyML.pointerEq;
|
wenzelm@29714
|
19 |
|
wenzelm@29714
|
20 |
fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
|
wenzelm@29714
|
21 |
|
wenzelm@29714
|
22 |
|
wenzelm@29714
|
23 |
(* runtime compilation *)
|
wenzelm@29714
|
24 |
|
wenzelm@29714
|
25 |
local
|
wenzelm@29714
|
26 |
|
wenzelm@29714
|
27 |
fun drop_newline s =
|
wenzelm@29714
|
28 |
if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
|
wenzelm@29714
|
29 |
else s;
|
wenzelm@29714
|
30 |
|
wenzelm@29714
|
31 |
in
|
wenzelm@29714
|
32 |
|
wenzelm@30688
|
33 |
fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
|
wenzelm@30688
|
34 |
(start_line, name) verbose txt =
|
wenzelm@29714
|
35 |
let
|
wenzelm@29714
|
36 |
val current_line = ref start_line;
|
wenzelm@30688
|
37 |
val in_buffer = ref (String.explode (tune_source txt));
|
wenzelm@29714
|
38 |
val out_buffer = ref ([]: string list);
|
wenzelm@29714
|
39 |
fun output () = drop_newline (implode (rev (! out_buffer)));
|
wenzelm@29714
|
40 |
|
wenzelm@29714
|
41 |
fun get () =
|
wenzelm@29714
|
42 |
(case ! in_buffer of
|
wenzelm@29714
|
43 |
[] => NONE
|
wenzelm@29714
|
44 |
| c :: cs =>
|
wenzelm@29714
|
45 |
(in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
|
wenzelm@29714
|
46 |
fun put s = out_buffer := s :: ! out_buffer;
|
wenzelm@30688
|
47 |
fun put_message {message = msg1, hard, location = {startLine = line, ...}, context} =
|
wenzelm@30205
|
48 |
(put (if hard then "Error: " else "Warning: ");
|
wenzelm@30688
|
49 |
PolyML.prettyPrint (put, 76) msg1;
|
wenzelm@30688
|
50 |
(case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2);
|
wenzelm@30688
|
51 |
put ("At" ^ str_of_pos line name ^ "\n"));
|
wenzelm@29714
|
52 |
|
wenzelm@29714
|
53 |
val parameters =
|
wenzelm@29714
|
54 |
[PolyML.Compiler.CPOutStream put,
|
wenzelm@29714
|
55 |
PolyML.Compiler.CPLineNo (fn () => ! current_line),
|
wenzelm@29714
|
56 |
PolyML.Compiler.CPErrorMessageProc put_message,
|
wenzelm@30205
|
57 |
PolyML.Compiler.CPNameSpace name_space,
|
wenzelm@30205
|
58 |
PolyML.Compiler.CPPrintInAlphabeticalOrder false];
|
wenzelm@29714
|
59 |
val _ =
|
wenzelm@29714
|
60 |
(while not (List.null (! in_buffer)) do
|
wenzelm@29714
|
61 |
PolyML.compiler (get, parameters) ())
|
wenzelm@29714
|
62 |
handle exn =>
|
wenzelm@29714
|
63 |
(put ("Exception- " ^ General.exnMessage exn ^ " raised");
|
wenzelm@30688
|
64 |
error (output ()); raise exn);
|
wenzelm@29714
|
65 |
in if verbose then print (output ()) else () end;
|
wenzelm@29714
|
66 |
|
wenzelm@30688
|
67 |
fun use_file context verbose name =
|
wenzelm@29714
|
68 |
let
|
wenzelm@29714
|
69 |
val instream = TextIO.openIn name;
|
wenzelm@29714
|
70 |
val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
|
wenzelm@30688
|
71 |
in use_text context (1, name) verbose txt end;
|
wenzelm@29714
|
72 |
|
wenzelm@29714
|
73 |
end;
|
wenzelm@30629
|
74 |
|
wenzelm@30629
|
75 |
|
wenzelm@30629
|
76 |
(* toplevel pretty printing *)
|
wenzelm@30629
|
77 |
|
wenzelm@30691
|
78 |
val pretty_ml =
|
wenzelm@30691
|
79 |
let
|
wenzelm@30691
|
80 |
fun convert len (PrettyBlock (ind, _, context, prts)) =
|
wenzelm@30691
|
81 |
let
|
wenzelm@30691
|
82 |
fun property name default =
|
wenzelm@30691
|
83 |
(case List.find (fn ContextProperty (a, _) => name = a | _ => false) context of
|
wenzelm@30691
|
84 |
SOME (ContextProperty (_, b)) => b
|
wenzelm@30691
|
85 |
| NONE => default);
|
wenzelm@30691
|
86 |
val bg = property "begin" "";
|
wenzelm@30691
|
87 |
val en = property "end" "";
|
wenzelm@30691
|
88 |
val len' = property "length" len;
|
wenzelm@30691
|
89 |
in ML_Pretty.Block ((bg, en), map (convert len') prts, ind) end
|
wenzelm@30691
|
90 |
| convert len (PrettyString s) =
|
wenzelm@30691
|
91 |
ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s)
|
wenzelm@30691
|
92 |
| convert _ (PrettyBreak (wd, _)) =
|
wenzelm@30691
|
93 |
ML_Pretty.Break (if wd < 99999 then (false, wd) else (true, 2));
|
wenzelm@30691
|
94 |
in convert "" end;
|
wenzelm@30642
|
95 |
|
wenzelm@30691
|
96 |
fun ml_pretty (ML_Pretty.Block ((bg, en), prts, ind)) =
|
wenzelm@30694
|
97 |
let val context =
|
wenzelm@30694
|
98 |
(if bg = "" then [] else [ContextProperty ("begin", bg)]) @
|
wenzelm@30694
|
99 |
(if en = "" then [] else [ContextProperty ("end", en)])
|
wenzelm@30694
|
100 |
in PrettyBlock (ind, false, context, map ml_pretty prts) end
|
wenzelm@30691
|
101 |
| ml_pretty (ML_Pretty.String (s, len)) =
|
wenzelm@30691
|
102 |
if len = size s then PrettyString s
|
wenzelm@30691
|
103 |
else PrettyBlock (0, false, [ContextProperty ("length", Int.toString len)], [PrettyString s])
|
wenzelm@30629
|
104 |
| ml_pretty (ML_Pretty.Break (false, wd)) = PrettyBreak (wd, 0)
|
wenzelm@30629
|
105 |
| ml_pretty (ML_Pretty.Break (true, _)) = PrettyBreak (99999, 0);
|
wenzelm@30629
|
106 |
|
wenzelm@30688
|
107 |
fun toplevel_pp context (_: string list) pp =
|
wenzelm@30688
|
108 |
use_text context (1, "pp") false
|
wenzelm@30629
|
109 |
("addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
|
wenzelm@30629
|
110 |
|