equal
deleted
inserted
replaced
1 (* Title: Pure/ML-Systems/polyml_old_compiler4.ML |
1 (* Title: Pure/ML-Systems/polyml_old_compiler4.ML |
2 |
2 |
3 Runtime compilation -- for old PolyML.compiler (version 4.x). |
3 Runtime compilation -- for old PolyML.compiler (version 4.x). |
4 *) |
4 *) |
5 |
5 |
6 fun use_text (tune: string -> string) _ _ (line: int, name) (print, err) verbose txt = |
6 fun use_text ({tune_source, print, error, ...}: use_context) (line: int, name) verbose txt = |
7 let |
7 let |
8 val in_buffer = ref (explode (tune txt)); |
8 val in_buffer = ref (explode (tune_source txt)); |
9 val out_buffer = ref ([]: string list); |
9 val out_buffer = ref ([]: string list); |
10 fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs)); |
10 fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs)); |
11 |
11 |
12 fun get () = |
12 fun get () = |
13 (case ! in_buffer of |
13 (case ! in_buffer of |
19 (case ! in_buffer of |
19 (case ! in_buffer of |
20 [] => () |
20 [] => () |
21 | _ => (PolyML.compiler (get, put) (); exec ())); |
21 | _ => (PolyML.compiler (get, put) (); exec ())); |
22 in |
22 in |
23 exec () handle exn => |
23 exec () handle exn => |
24 (err ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn); |
24 (error ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn); |
25 if verbose then print (output ()) else () |
25 if verbose then print (output ()) else () |
26 end; |
26 end; |
27 |
27 |
28 fun use_file tune str_of_pos name_space output verbose name = |
28 fun use_file context verbose name = |
29 let |
29 let |
30 val instream = TextIO.openIn name; |
30 val instream = TextIO.openIn name; |
31 val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream); |
31 val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream); |
32 in use_text tune str_of_pos name_space (1, name) output verbose txt end; |
32 in use_text context (1, name) verbose txt end; |