author | wenzelm |
Mon, 19 Jan 2009 19:38:03 +0100 | |
changeset 29564 | f8b933a62151 |
parent 28268 | ac8431ecd57e |
child 30687 | beaadd5af500 |
permissions | -rw-r--r-- |
wenzelm@26382 | 1 |
(* Title: Pure/ML-Systems/polyml_old_compiler4.ML |
wenzelm@26382 | 2 |
|
wenzelm@26385 | 3 |
Runtime compilation -- for old PolyML.compiler (version 4.x). |
wenzelm@26382 | 4 |
*) |
wenzelm@26382 | 5 |
|
wenzelm@28268 | 6 |
fun use_text (tune: string -> string) _ _ (line: int, name) (print, err) verbose txt = |
wenzelm@26382 | 7 |
let |
wenzelm@26382 | 8 |
val in_buffer = ref (explode (tune txt)); |
wenzelm@26382 | 9 |
val out_buffer = ref ([]: string list); |
wenzelm@26382 | 10 |
fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs)); |
wenzelm@26382 | 11 |
|
wenzelm@26382 | 12 |
fun get () = |
wenzelm@26382 | 13 |
(case ! in_buffer of |
wenzelm@26382 | 14 |
[] => "" |
wenzelm@26382 | 15 |
| c :: cs => (in_buffer := cs; c)); |
wenzelm@26382 | 16 |
fun put s = out_buffer := s :: ! out_buffer; |
wenzelm@26382 | 17 |
|
wenzelm@26382 | 18 |
fun exec () = |
wenzelm@26382 | 19 |
(case ! in_buffer of |
wenzelm@26382 | 20 |
[] => () |
wenzelm@26382 | 21 |
| _ => (PolyML.compiler (get, put) (); exec ())); |
wenzelm@26382 | 22 |
in |
wenzelm@26382 | 23 |
exec () handle exn => |
wenzelm@26382 | 24 |
(err ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn); |
wenzelm@26382 | 25 |
if verbose then print (output ()) else () |
wenzelm@26382 | 26 |
end; |
wenzelm@26382 | 27 |
|
wenzelm@28268 | 28 |
fun use_file tune str_of_pos name_space output verbose name = |
wenzelm@26382 | 29 |
let |
wenzelm@26382 | 30 |
val instream = TextIO.openIn name; |
wenzelm@26504 | 31 |
val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream); |
wenzelm@28268 | 32 |
in use_text tune str_of_pos name_space (1, name) output verbose txt end; |