1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/ML-Systems/polyml_old_compiler4.ML	Mon Mar 24 18:35:48 2008 +0100
     1.3 @@ -0,0 +1,34 @@
     1.4 +(*  Title:      Pure/ML-Systems/polyml_old_compiler4.ML
     1.5 +    ID:         $Id$
     1.6 +
     1.7 +Runtime compilation -- for old version of PolyML.compiler (version 4.x).
     1.8 +*)
     1.9 +
    1.10 +fun use_text (tune: string -> string) name (print, err) verbose txt =
    1.11 +  let
    1.12 +    val in_buffer = ref (explode (tune txt));
    1.13 +    val out_buffer = ref ([]: string list);
    1.14 +    fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
    1.15 +
    1.16 +    fun get () =
    1.17 +      (case ! in_buffer of
    1.18 +        [] => ""
    1.19 +      | c :: cs => (in_buffer := cs; c));
    1.20 +    fun put s = out_buffer := s :: ! out_buffer;
    1.21 +
    1.22 +    fun exec () =
    1.23 +      (case ! in_buffer of
    1.24 +        [] => ()
    1.25 +      | _ => (PolyML.compiler (get, put) (); exec ()));
    1.26 +  in
    1.27 +    exec () handle exn =>
    1.28 +      (err ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
    1.29 +    if verbose then print (output ()) else ()
    1.30 +  end;
    1.31 +
    1.32 +fun use_file tune output verbose name =
    1.33 +  let
    1.34 +    val instream = TextIO.openIn name;
    1.35 +    val txt = TextIO.inputAll instream before TextIO.closeIn instream;
    1.36 +  in use_text tune name output verbose txt end;
    1.37 +