equal
deleted
inserted
replaced
|
1 (* Title: Pure/ML-Systems/polyml-5.0.ML |
|
2 ID: $Id$ |
|
3 |
|
4 Compatibility wrapper for Poly/ML 5.1. |
|
5 *) |
|
6 |
|
7 use "ML-Systems/polyml.ML"; |
|
8 |
|
9 val pointer_eq = PolyML.pointerEq; |
|
10 |
|
11 |
|
12 (* improved versions of use_text/file *) |
|
13 |
|
14 fun use_text name (print, err) verbose txt = |
|
15 let |
|
16 val in_buffer = ref (explode txt); |
|
17 val out_buffer = ref ([]: string list); |
|
18 fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs)); |
|
19 |
|
20 val line_no = ref 1; |
|
21 fun line () = ! line_no; |
|
22 fun get () = |
|
23 (case ! in_buffer of |
|
24 [] => "" |
|
25 | c :: cs => (in_buffer := cs; if c = "\n" then line_no := ! line_no + 1 else (); c)); |
|
26 fun put s = out_buffer := s :: ! out_buffer; |
|
27 |
|
28 fun exec () = |
|
29 (case ! in_buffer of |
|
30 [] => () |
|
31 | _ => (PolyML.compilerEx (get, put, line, name) (); exec ())); |
|
32 in |
|
33 exec () handle exn => (err (output ()); raise exn); |
|
34 if verbose then print (output ()) else () |
|
35 end; |
|
36 |
|
37 fun use_file output verbose name = |
|
38 let |
|
39 val instream = TextIO.openIn name; |
|
40 val txt = TextIO.inputAll instream before TextIO.closeIn instream; |
|
41 in use_text name output verbose txt end; |