moved use_text/file to polyml_old_compiler5.ML;
authorwenzelm
Mon Mar 24 18:35:42 2008 +0100 (2008-03-24 ago)
changeset 26378bac8d5e5f833
parent 26377 54dc2f9c5be8
child 26379 a01a05cdd3b8
moved use_text/file to polyml_old_compiler5.ML;
src/Pure/ML-Systems/polyml-5.0.ML
     1.1 --- a/src/Pure/ML-Systems/polyml-5.0.ML	Mon Mar 24 18:35:41 2008 +0100
     1.2 +++ b/src/Pure/ML-Systems/polyml-5.0.ML	Mon Mar 24 18:35:42 2008 +0100
     1.3 @@ -5,37 +5,7 @@
     1.4  *)
     1.5  
     1.6  use "ML-Systems/polyml_common.ML";
     1.7 +use "ML-Systems/polyml_old_compiler5.ML";
     1.8  
     1.9  val pointer_eq = PolyML.pointerEq;
    1.10  
    1.11 -
    1.12 -(* improved versions of use_text/file *)
    1.13 -
    1.14 -fun use_text (tune: string -> string) name (print, err) verbose txt =
    1.15 -  let
    1.16 -    val in_buffer = ref (explode (tune txt));
    1.17 -    val out_buffer = ref ([]: string list);
    1.18 -    fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
    1.19 -
    1.20 -    val line_no = ref 1;
    1.21 -    fun line () = ! line_no;
    1.22 -    fun get () =
    1.23 -      (case ! in_buffer of
    1.24 -        [] => ""
    1.25 -      | c :: cs => (in_buffer := cs; if c = "\n" then line_no := ! line_no + 1 else (); c));
    1.26 -    fun put s = out_buffer := s :: ! out_buffer;
    1.27 -
    1.28 -    fun exec () =
    1.29 -      (case ! in_buffer of
    1.30 -        [] => ()
    1.31 -      | _ => (PolyML.compilerEx (get, put, line, name) (); exec ()));
    1.32 -  in
    1.33 -    exec () handle exn => (err (output ()); raise exn);
    1.34 -    if verbose then print (output ()) else ()
    1.35 -  end;
    1.36 -
    1.37 -fun use_file tune output verbose name =
    1.38 -  let
    1.39 -    val instream = TextIO.openIn name;
    1.40 -    val txt = TextIO.inputAll instream before TextIO.closeIn instream;
    1.41 -  in use_text tune name output verbose txt end;