|
1 (* Title: Pure/ML-Systems/polyml.ML |
|
2 |
|
3 Compatibility wrapper for experimental versions of Poly/ML after 5.2.1. |
|
4 *) |
|
5 |
|
6 open Thread; |
|
7 use "ML-Systems/polyml_common.ML"; |
|
8 use "ML-Systems/multithreading_polyml.ML"; |
|
9 |
|
10 val pointer_eq = PolyML.pointerEq; |
|
11 |
|
12 fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction; |
|
13 |
|
14 |
|
15 (* toplevel pretty printers *) |
|
16 |
|
17 (*dummy version*) |
|
18 fun make_pp path pprint = (); |
|
19 fun install_pp _ = (); |
|
20 |
|
21 |
|
22 (* runtime compilation *) |
|
23 |
|
24 structure ML_NameSpace = |
|
25 struct |
|
26 open PolyML.NameSpace; |
|
27 val global = PolyML.globalNameSpace; |
|
28 end; |
|
29 |
|
30 local |
|
31 |
|
32 fun drop_newline s = |
|
33 if String.isSuffix "\n" s then String.substring (s, 0, size s - 1) |
|
34 else s; |
|
35 |
|
36 in |
|
37 |
|
38 fun use_text (tune: string -> string) str_of_pos |
|
39 name_space (start_line, name) (print, err) verbose txt = |
|
40 let |
|
41 val current_line = ref start_line; |
|
42 val in_buffer = ref (String.explode (tune txt)); |
|
43 val out_buffer = ref ([]: string list); |
|
44 fun output () = drop_newline (implode (rev (! out_buffer))); |
|
45 |
|
46 fun get () = |
|
47 (case ! in_buffer of |
|
48 [] => NONE |
|
49 | c :: cs => |
|
50 (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c)); |
|
51 fun put s = out_buffer := s :: ! out_buffer; |
|
52 fun put_message (prt, is_err, {file, line, offset}) = |
|
53 (put (if is_err then "Error: " else "Warning: "); |
|
54 PolyML.prettyPrint (put, 76) prt; |
|
55 put (str_of_pos line name ^ "\n")); |
|
56 |
|
57 val parameters = |
|
58 [PolyML.Compiler.CPOutStream put, |
|
59 PolyML.Compiler.CPLineNo (fn () => ! current_line), |
|
60 PolyML.Compiler.CPErrorMessageProc put_message, |
|
61 PolyML.Compiler.CPNameSpace name_space]; |
|
62 val _ = |
|
63 (while not (List.null (! in_buffer)) do |
|
64 PolyML.compiler (get, parameters) ()) |
|
65 handle exn => |
|
66 (put ("Exception- " ^ General.exnMessage exn ^ " raised"); |
|
67 err (output ()); raise exn); |
|
68 in if verbose then print (output ()) else () end; |
|
69 |
|
70 fun use_file tune str_of_pos name_space output verbose name = |
|
71 let |
|
72 val instream = TextIO.openIn name; |
|
73 val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream); |
|
74 in use_text tune str_of_pos name_space (1, name) output verbose txt end; |
|
75 |
|
76 end; |