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) name (print, err) verbose txt = |
26 let |
26 let |
27 val in_buffer = ref (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 line_no = ref 1; |
32 fun line () = ! line_no; |
32 fun line () = ! line_no; |
33 fun get () = |
33 fun get () = |
34 (case ! in_buffer of |
34 (case ! in_buffer of |
35 [] => "" |
35 [] => NONE |
36 | c :: cs => (in_buffer := cs; if c = "\n" then line_no := ! line_no + 1 else (); c)); |
36 | c :: cs => (in_buffer := cs; if c = #"\n" then line_no := ! line_no + 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 fun exec () = |
39 val _ = |
40 (case ! in_buffer of |
40 (while not (List.null (! in_buffer)) do |
41 [] => () |
41 PolyML.compiler |
42 | _ => (PolyML.compilerEx (get, put, line, name) (); exec ())); |
42 {getChar = get, putString = put, lineNumber = line, fileName = name, |
|
43 nameSpace = PolyML.globalNameSpace} ()) |
|
44 handle exn => (err (output ()); raise exn); |
43 in |
45 in |
44 exec () handle exn => (err (output ()); raise exn); |
|
45 if verbose then print (output ()) else () |
46 if verbose then print (output ()) else () |
46 end; |
47 end; |
47 |
48 |
48 fun use_file tune output verbose name = |
49 fun use_file tune output verbose name = |
49 let |
50 let |
50 val instream = TextIO.openIn name; |
51 val instream = TextIO.openIn name; |
51 val txt = TextIO.inputAll instream before TextIO.closeIn instream; |
52 val txt = TextIO.inputAll instream before TextIO.closeIn instream; |
52 in use_text tune name output verbose txt end; |
53 in use_text tune name output verbose txt end; |
|
54 |