20 end; |
20 end; |
21 |
21 |
22 |
22 |
23 (* improved versions of use_text/file *) |
23 (* improved versions of use_text/file *) |
24 |
24 |
25 fun use_text (tune: string -> string) name (print, err) verbose txt = |
25 fun use_text (tune: string -> string) (line, name) (print, err) verbose txt = |
26 let |
26 let |
27 val in_buffer = ref (String.explode (tune txt)); |
27 val in_buffer = ref (String.explode (tune txt)); |
28 val out_buffer = ref ([]: string list); |
28 val out_buffer = ref ([]: string list); |
29 fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs)); |
29 fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs)); |
30 |
30 |
31 val line_no = ref 1; |
31 val current_line = ref line; |
32 fun line () = ! line_no; |
|
33 fun get () = |
32 fun get () = |
34 (case ! in_buffer of |
33 (case ! in_buffer of |
35 [] => NONE |
34 [] => NONE |
36 | c :: cs => (in_buffer := cs; if c = #"\n" then line_no := ! line_no + 1 else (); SOME c)); |
35 | c :: cs => |
|
36 (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c)); |
37 fun put s = out_buffer := s :: ! out_buffer; |
37 fun put s = out_buffer := s :: ! out_buffer; |
38 |
38 |
39 val _ = |
39 val _ = |
40 (while not (List.null (! in_buffer)) do |
40 (while not (List.null (! in_buffer)) do |
41 PolyML.compiler |
41 PolyML.compiler |
42 {getChar = get, putString = put, lineNumber = line, fileName = name, |
42 {getChar = get, putString = put, lineNumber = fn () => ! current_line, fileName = name, |
43 nameSpace = PolyML.globalNameSpace} ()) |
43 nameSpace = PolyML.globalNameSpace} ()) |
44 handle exn => (err (output ()); raise exn); |
44 handle exn => (err (output ()); raise exn); |
45 in |
45 in |
46 if verbose then print (output ()) else () |
46 if verbose then print (output ()) else () |
47 end; |
47 end; |
48 |
48 |
49 fun use_file tune output verbose name = |
49 fun use_file tune output verbose name = |
50 let |
50 let |
51 val instream = TextIO.openIn name; |
51 val instream = TextIO.openIn name; |
52 val txt = TextIO.inputAll instream before TextIO.closeIn instream; |
52 val txt = TextIO.inputAll instream before TextIO.closeIn instream; |
53 in use_text tune name output verbose txt end; |
53 in use_text tune (1, name) output verbose txt end; |
54 |
54 |