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