equal
deleted
inserted
replaced
10 val pointer_eq = PolyML.pointerEq; |
10 val pointer_eq = PolyML.pointerEq; |
11 |
11 |
12 |
12 |
13 (* improved versions of use_text/file *) |
13 (* improved versions of use_text/file *) |
14 |
14 |
15 fun use_text name (print, err) verbose txt = |
15 fun use_text (tune: string -> string) name (print, err) verbose txt = |
16 let |
16 let |
17 val in_buffer = ref (explode txt); |
17 val in_buffer = ref (explode (tune txt)); |
18 val out_buffer = ref ([]: string list); |
18 val out_buffer = ref ([]: string list); |
19 fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs)); |
19 fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs)); |
20 |
20 |
21 val line_no = ref 1; |
21 val line_no = ref 1; |
22 fun line () = ! line_no; |
22 fun line () = ! line_no; |
33 in |
33 in |
34 exec () handle exn => (err (output ()); raise exn); |
34 exec () handle exn => (err (output ()); raise exn); |
35 if verbose then print (output ()) else () |
35 if verbose then print (output ()) else () |
36 end; |
36 end; |
37 |
37 |
38 fun use_file output verbose name = |
38 fun use_file tune output verbose name = |
39 let |
39 let |
40 val instream = TextIO.openIn name; |
40 val instream = TextIO.openIn name; |
41 val txt = TextIO.inputAll instream before TextIO.closeIn instream; |
41 val txt = TextIO.inputAll instream before TextIO.closeIn instream; |
42 in use_text name output verbose txt end; |
42 in use_text tune name output verbose txt end; |