# HG changeset patch
# User wenzelm
# Date 1165860325 -3600
# Node ID 148c8aba89ddc4945fadbd9d06ad9ed4bd5c07ee
# Parent  ea6f846d8c4ba63981bf8625950e3ddadf34de57
added improved versions of use_text/file (still inactive);

diff -r ea6f846d8c4b -r 148c8aba89dd src/Pure/ML-Systems/polyml-5.0.ML
--- a/src/Pure/ML-Systems/polyml-5.0.ML	Mon Dec 11 19:05:23 2006 +0100
+++ b/src/Pure/ML-Systems/polyml-5.0.ML	Mon Dec 11 19:05:25 2006 +0100
@@ -8,3 +8,44 @@
 use "ML-Systems/polyml.ML";
 
 val pointer_eq = PolyML.pointerEq;
+
+
+(* improved versions of use_text/file *)
+(*
+local
+
+fun use_ml name (print, err) verbose txt =
+  let
+    val in_buffer = ref (explode 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;
+
+in
+
+fun use_text output = use_ml "ML text" output;
+
+fun use_file output verbose name =
+  let
+    val instream = TextIO.openIn name;
+    val txt = TextIO.inputAll instream before TextIO.closeIn instream;
+  in use_ml name output verbose txt end;
+
+end;
+*)