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 local |
15 fun use_text name (print, err) verbose txt = |
16 |
|
17 fun use_ml name (print, err) verbose txt = |
|
18 let |
16 let |
19 val in_buffer = ref (explode txt); |
17 val in_buffer = ref (explode txt); |
20 val out_buffer = ref ([]: string list); |
18 val out_buffer = ref ([]: string list); |
21 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)); |
22 |
20 |
35 in |
33 in |
36 exec () handle exn => (err (output ()); raise exn); |
34 exec () handle exn => (err (output ()); raise exn); |
37 if verbose then print (output ()) else () |
35 if verbose then print (output ()) else () |
38 end; |
36 end; |
39 |
37 |
40 in |
|
41 |
|
42 fun use_text output = use_ml "ML text" output; |
|
43 |
|
44 fun use_file output verbose name = |
38 fun use_file output verbose name = |
45 let |
39 let |
46 val instream = TextIO.openIn name; |
40 val instream = TextIO.openIn name; |
47 val txt = TextIO.inputAll instream before TextIO.closeIn instream; |
41 val txt = TextIO.inputAll instream before TextIO.closeIn instream; |
48 in use_ml name output verbose txt end; |
42 in use_text name output verbose txt end; |
49 |
|
50 end; |
|