# HG changeset patch # User wenzelm # Date 1206380142 -3600 # Node ID bac8d5e5f833464e15ca5705ed4c2348f35a8ad9 # Parent 54dc2f9c5be8880e4a9b1cf6617f193a586c61b6 moved use_text/file to polyml_old_compiler5.ML; diff -r 54dc2f9c5be8 -r bac8d5e5f833 src/Pure/ML-Systems/polyml-5.0.ML --- a/src/Pure/ML-Systems/polyml-5.0.ML Mon Mar 24 18:35:41 2008 +0100 +++ b/src/Pure/ML-Systems/polyml-5.0.ML Mon Mar 24 18:35:42 2008 +0100 @@ -5,37 +5,7 @@ *) use "ML-Systems/polyml_common.ML"; +use "ML-Systems/polyml_old_compiler5.ML"; val pointer_eq = PolyML.pointerEq; - -(* improved versions of use_text/file *) - -fun use_text (tune: string -> string) name (print, err) verbose txt = - let - val in_buffer = ref (explode (tune txt)); - val out_buffer = ref ([]: string list); - fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs)); - - val line_no = ref 1; - fun line () = ! line_no; - fun get () = - (case ! in_buffer of - [] => "" - | c :: cs => (in_buffer := cs; if c = "\n" then line_no := ! line_no + 1 else (); c)); - fun put s = out_buffer := s :: ! out_buffer; - - fun exec () = - (case ! in_buffer of - [] => () - | _ => (PolyML.compilerEx (get, put, line, name) (); exec ())); - in - exec () handle exn => (err (output ()); raise exn); - if verbose then print (output ()) else () - end; - -fun use_file tune output verbose name = - let - val instream = TextIO.openIn name; - val txt = TextIO.inputAll instream before TextIO.closeIn instream; - in use_text tune name output verbose txt end;