equal
deleted
inserted
replaced
6 |
6 |
7 use "ML-Systems/polyml-4.1.4-patch.ML"; |
7 use "ML-Systems/polyml-4.1.4-patch.ML"; |
8 use "ML-Systems/polyml.ML"; |
8 use "ML-Systems/polyml.ML"; |
9 |
9 |
10 val pointer_eq = PolyML.pointerEq; |
10 val pointer_eq = PolyML.pointerEq; |
|
11 |
|
12 |
|
13 (* improved versions of use_text/file *) |
|
14 (* |
|
15 local |
|
16 |
|
17 fun use_ml name (print, err) verbose txt = |
|
18 let |
|
19 val in_buffer = ref (explode txt); |
|
20 val out_buffer = ref ([]: string list); |
|
21 fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs)); |
|
22 |
|
23 val line_no = ref 1; |
|
24 fun line () = ! line_no; |
|
25 fun get () = |
|
26 (case ! in_buffer of |
|
27 [] => "" |
|
28 | c :: cs => (in_buffer := cs; if c = "\n" then line_no := ! line_no + 1 else (); c)); |
|
29 fun put s = out_buffer := s :: ! out_buffer; |
|
30 |
|
31 fun exec () = |
|
32 (case ! in_buffer of |
|
33 [] => () |
|
34 | _ => (PolyML.compilerEx (get, put, line, name) (); exec ())); |
|
35 in |
|
36 exec () handle exn => (err (output ()); raise exn); |
|
37 if verbose then print (output ()) else () |
|
38 end; |
|
39 |
|
40 in |
|
41 |
|
42 fun use_text output = use_ml "ML text" output; |
|
43 |
|
44 fun use_file output verbose name = |
|
45 let |
|
46 val instream = TextIO.openIn name; |
|
47 val txt = TextIO.inputAll instream before TextIO.closeIn instream; |
|
48 in use_ml name output verbose txt end; |
|
49 |
|
50 end; |
|
51 *) |