equal
deleted
inserted
replaced
1 (* Title: Pure/ML-Systems/polyml_old_compiler4.ML |
1 (* Title: Pure/ML-Systems/polyml_old_compiler4.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 |
3 |
4 Runtime compilation -- for old version of PolyML.compiler (version 4.x). |
4 Runtime compilation -- for old PolyML.compiler (version 4.x). |
5 *) |
5 *) |
6 |
6 |
7 fun use_text (tune: string -> string) name (print, err) verbose txt = |
7 fun use_text (tune: string -> string) (line: int, name) (print, err) verbose txt = |
8 let |
8 let |
9 val in_buffer = ref (explode (tune txt)); |
9 val in_buffer = ref (explode (tune txt)); |
10 val out_buffer = ref ([]: string list); |
10 val out_buffer = ref ([]: string list); |
11 fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs)); |
11 fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs)); |
12 |
12 |
28 |
28 |
29 fun use_file tune output verbose name = |
29 fun use_file tune output verbose name = |
30 let |
30 let |
31 val instream = TextIO.openIn name; |
31 val instream = TextIO.openIn name; |
32 val txt = TextIO.inputAll instream before TextIO.closeIn instream; |
32 val txt = TextIO.inputAll instream before TextIO.closeIn instream; |
33 in use_text tune name output verbose txt end; |
33 in use_text tune (1, name) output verbose txt end; |
34 |
34 |