equal
deleted
inserted
replaced
32 in |
32 in |
33 exec () handle exn => (err (output ()); raise exn); |
33 exec () handle exn => (err (output ()); raise exn); |
34 if verbose then print (output ()) else () |
34 if verbose then print (output ()) else () |
35 end; |
35 end; |
36 |
36 |
37 fun use_file output verbose name = |
37 fun use_file tune output verbose name = |
38 let |
38 let |
39 val instream = TextIO.openIn name; |
39 val instream = TextIO.openIn name; |
40 val txt = TextIO.inputAll instream before TextIO.closeIn instream; |
40 val txt = TextIO.inputAll instream before TextIO.closeIn instream; |
41 in use_text name output verbose txt end; |
41 in use_text tune name output verbose txt end; |