2 |
2 |
3 Compatibility wrapper for experimental versions of Poly/ML after 5.2.1. |
3 Compatibility wrapper for experimental versions of Poly/ML after 5.2.1. |
4 *) |
4 *) |
5 |
5 |
6 open Thread; |
6 open Thread; |
|
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 |
7 use "ML-Systems/polyml_common.ML"; |
15 use "ML-Systems/polyml_common.ML"; |
8 use "ML-Systems/multithreading_polyml.ML"; |
16 use "ML-Systems/multithreading_polyml.ML"; |
9 |
17 |
10 val pointer_eq = PolyML.pointerEq; |
18 val pointer_eq = PolyML.pointerEq; |
11 |
19 |
12 fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction; |
20 fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction; |
13 |
21 |
14 |
22 |
15 (* runtime compilation *) |
23 (* runtime compilation *) |
16 |
24 |
17 structure ML_NameSpace = |
|
18 struct |
|
19 open PolyML.NameSpace; |
|
20 val global = PolyML.globalNameSpace; |
|
21 end; |
|
22 |
|
23 local |
25 local |
24 |
26 |
25 fun drop_newline s = |
27 fun drop_newline s = |
26 if String.isSuffix "\n" s then String.substring (s, 0, size s - 1) |
28 if String.isSuffix "\n" s then String.substring (s, 0, size s - 1) |
27 else s; |
29 else s; |
28 |
30 |
29 in |
31 in |
30 |
32 |
31 fun use_text (tune: string -> string) str_of_pos |
33 fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context) |
32 name_space (start_line, name) (print, err) verbose txt = |
34 (start_line, name) verbose txt = |
33 let |
35 let |
34 val current_line = ref start_line; |
36 val current_line = ref start_line; |
35 val in_buffer = ref (String.explode (tune txt)); |
37 val in_buffer = ref (String.explode (tune_source txt)); |
36 val out_buffer = ref ([]: string list); |
38 val out_buffer = ref ([]: string list); |
37 fun output () = drop_newline (implode (rev (! out_buffer))); |
39 fun output () = drop_newline (implode (rev (! out_buffer))); |
38 |
40 |
39 fun get () = |
41 fun get () = |
40 (case ! in_buffer of |
42 (case ! in_buffer of |
41 [] => NONE |
43 [] => NONE |
42 | c :: cs => |
44 | c :: cs => |
43 (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c)); |
45 (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c)); |
44 fun put s = out_buffer := s :: ! out_buffer; |
46 fun put s = out_buffer := s :: ! out_buffer; |
45 fun put_message {message, hard, location = {startLine = line, ...}, context} = |
47 fun put_message {message = msg1, hard, location = {startLine = line, ...}, context} = |
46 (put (if hard then "Error: " else "Warning: "); |
48 (put (if hard then "Error: " else "Warning: "); |
47 PolyML.prettyPrint (put, 76) message; |
49 PolyML.prettyPrint (put, 76) msg1; |
48 put (str_of_pos line name ^ "\n")); |
50 (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2); |
|
51 put ("At" ^ str_of_pos line name ^ "\n")); |
49 |
52 |
50 val parameters = |
53 val parameters = |
51 [PolyML.Compiler.CPOutStream put, |
54 [PolyML.Compiler.CPOutStream put, |
52 PolyML.Compiler.CPLineNo (fn () => ! current_line), |
55 PolyML.Compiler.CPLineNo (fn () => ! current_line), |
53 PolyML.Compiler.CPErrorMessageProc put_message, |
56 PolyML.Compiler.CPErrorMessageProc put_message, |
56 val _ = |
59 val _ = |
57 (while not (List.null (! in_buffer)) do |
60 (while not (List.null (! in_buffer)) do |
58 PolyML.compiler (get, parameters) ()) |
61 PolyML.compiler (get, parameters) ()) |
59 handle exn => |
62 handle exn => |
60 (put ("Exception- " ^ General.exnMessage exn ^ " raised"); |
63 (put ("Exception- " ^ General.exnMessage exn ^ " raised"); |
61 err (output ()); raise exn); |
64 error (output ()); raise exn); |
62 in if verbose then print (output ()) else () end; |
65 in if verbose then print (output ()) else () end; |
63 |
66 |
64 fun use_file tune str_of_pos name_space output verbose name = |
67 fun use_file context verbose name = |
65 let |
68 let |
66 val instream = TextIO.openIn name; |
69 val instream = TextIO.openIn name; |
67 val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream); |
70 val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream); |
68 in use_text tune str_of_pos name_space (1, name) output verbose txt end; |
71 in use_text context (1, name) verbose txt end; |
69 |
72 |
70 end; |
73 end; |
71 |
74 |
72 |
75 |
73 (* toplevel pretty printing *) |
76 (* toplevel pretty printing *) |
79 fun ml_pretty (ML_Pretty.Block (_, prts, ind)) = PrettyBlock (ind, false, [], map ml_pretty prts) |
82 fun ml_pretty (ML_Pretty.Block (_, prts, ind)) = PrettyBlock (ind, false, [], map ml_pretty prts) |
80 | ml_pretty (ML_Pretty.String (s, _)) = PrettyString s |
83 | ml_pretty (ML_Pretty.String (s, _)) = PrettyString s |
81 | ml_pretty (ML_Pretty.Break (false, wd)) = PrettyBreak (wd, 0) |
84 | ml_pretty (ML_Pretty.Break (false, wd)) = PrettyBreak (wd, 0) |
82 | ml_pretty (ML_Pretty.Break (true, _)) = PrettyBreak (99999, 0); |
85 | ml_pretty (ML_Pretty.Break (true, _)) = PrettyBreak (99999, 0); |
83 |
86 |
84 fun toplevel_pp tune str_of_pos output (_: string list) pp = |
87 fun toplevel_pp context (_: string list) pp = |
85 use_text tune str_of_pos ML_NameSpace.global (1, "pp") output false |
88 use_text context (1, "pp") false |
86 ("addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))"); |
89 ("addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))"); |
87 |
90 |