11 val pointer_eq = PolyML.pointerEq; |
11 val pointer_eq = PolyML.pointerEq; |
12 |
12 |
13 |
13 |
14 (* runtime compilation *) |
14 (* runtime compilation *) |
15 |
15 |
|
16 structure ML_NameSpace = |
|
17 struct |
|
18 open PolyML.NameSpace; |
|
19 val global = PolyML.globalNameSpace; |
|
20 end; |
|
21 |
16 local |
22 local |
17 |
23 |
18 fun drop_newline s = |
24 fun drop_newline s = |
19 if String.isSuffix "\n" s then String.substring (s, 0, size s - 1) |
25 if String.isSuffix "\n" s then String.substring (s, 0, size s - 1) |
20 else s; |
26 else s; |
21 |
27 |
22 in |
28 in |
23 |
29 |
24 fun use_text (tune: string -> string) str_of_pos (start_line, name) (print, err) verbose txt = |
30 fun use_text (tune: string -> string) str_of_pos |
|
31 name_space (start_line, name) (print, err) verbose txt = |
25 let |
32 let |
26 val current_line = ref start_line; |
33 val current_line = ref start_line; |
27 val in_buffer = ref (String.explode (tune txt)); |
34 val in_buffer = ref (String.explode (tune txt)); |
28 val out_buffer = ref ([]: string list); |
35 val out_buffer = ref ([]: string list); |
29 fun output () = drop_newline (implode (rev (! out_buffer))); |
36 fun output () = drop_newline (implode (rev (! out_buffer))); |
38 (if is_err then "Error: " else "Warning: ") ^ drop_newline msg ^ str_of_pos line name ^ "\n"; |
45 (if is_err then "Error: " else "Warning: ") ^ drop_newline msg ^ str_of_pos line name ^ "\n"; |
39 |
46 |
40 val parameters = |
47 val parameters = |
41 [PolyML.Compiler.CPOutStream put, |
48 [PolyML.Compiler.CPOutStream put, |
42 PolyML.Compiler.CPLineNo (fn () => ! current_line), |
49 PolyML.Compiler.CPLineNo (fn () => ! current_line), |
43 PolyML.Compiler.CPErrorMessageProc (put o message)]; |
50 PolyML.Compiler.CPErrorMessageProc (put o message), |
|
51 PolyML.Compiler.CPNameSpace name_space]; |
44 val _ = |
52 val _ = |
45 (while not (List.null (! in_buffer)) do |
53 (while not (List.null (! in_buffer)) do |
46 PolyML.compiler (get, parameters) ()) |
54 PolyML.compiler (get, parameters) ()) |
47 handle exn => |
55 handle exn => |
48 (put ("Exception- " ^ General.exnMessage exn ^ " raised"); |
56 (put ("Exception- " ^ General.exnMessage exn ^ " raised"); |
49 err (output ()); raise exn); |
57 err (output ()); raise exn); |
50 in if verbose then print (output ()) else () end; |
58 in if verbose then print (output ()) else () end; |
51 |
59 |
52 fun use_file tune str_of_pos output verbose name = |
60 fun use_file tune str_of_pos name_space output verbose name = |
53 let |
61 let |
54 val instream = TextIO.openIn name; |
62 val instream = TextIO.openIn name; |
55 val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream); |
63 val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream); |
56 in use_text tune str_of_pos (1, name) output verbose txt end; |
64 in use_text tune str_of_pos name_space (1, name) output verbose txt end; |
57 |
65 |
58 end; |
66 end; |