1.1 --- a/src/Pure/ML-Systems/polyml_old_compiler4.ML	Sat May 30 22:37:38 2009 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,32 +0,0 @@
     1.4 -(*  Title:      Pure/ML-Systems/polyml_old_compiler4.ML
     1.5 -
     1.6 -Runtime compilation -- for old PolyML.compiler (version 4.x).
     1.7 -*)
     1.8 -
     1.9 -fun use_text ({tune_source, print, error, ...}: use_context) (line: int, name) verbose txt =
    1.10 -  let
    1.11 -    val in_buffer = ref (explode (tune_source txt));
    1.12 -    val out_buffer = ref ([]: string list);
    1.13 -    fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
    1.14 -
    1.15 -    fun get () =
    1.16 -      (case ! in_buffer of
    1.17 -        [] => ""
    1.18 -      | c :: cs => (in_buffer := cs; c));
    1.19 -    fun put s = out_buffer := s :: ! out_buffer;
    1.20 -
    1.21 -    fun exec () =
    1.22 -      (case ! in_buffer of
    1.23 -        [] => ()
    1.24 -      | _ => (PolyML.compiler (get, put) (); exec ()));
    1.25 -  in
    1.26 -    exec () handle exn =>
    1.27 -      (error ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
    1.28 -    if verbose then print (output ()) else ()
    1.29 -  end;
    1.30 -
    1.31 -fun use_file context verbose name =
    1.32 -  let
    1.33 -    val instream = TextIO.openIn name;
    1.34 -    val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
    1.35 -  in use_text context (1, name) verbose txt end;