# HG changeset patch
# User wenzelm
# Date 897901560 -7200
# Node ID 301c37df931d60f2e853eaa0cf2b812db3258547
# Parent  224887671646df66867f5c786aa0b64062154bce
use_text replaces use_strings;

diff -r 224887671646 -r 301c37df931d src/Pure/ML-Systems/mlworks.ML
--- a/src/Pure/ML-Systems/mlworks.ML	Mon Jun 15 11:05:25 1998 +0200
+++ b/src/Pure/ML-Systems/mlworks.ML	Mon Jun 15 11:06:00 1998 +0200
@@ -66,14 +66,15 @@
 (* ML command execution *)
 
 (*Can one redirect 'use' directly to an instream?*)
-fun use_strings strs =
+fun use_text txt =
   let
     val tmp_name = OS.FileSys.tmpName ();
     val tmp_file = TextIO.openOut tmp_name;
-  in app (fn s => TextIO.output (tmp_file, s)) strs;
-     TextIO.closeOut tmp_file;
-     use tmp_name;
-     OS.FileSys.remove tmp_name
+  in
+    TextIO.output (tmp_file, txt);
+    TextIO.closeOut tmp_file;
+    use tmp_name;
+    OS.FileSys.remove tmp_name
   end;
 
 
diff -r 224887671646 -r 301c37df931d src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Mon Jun 15 11:05:25 1998 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Mon Jun 15 11:06:00 1998 +0200
@@ -41,22 +41,18 @@
 
 (* ML command execution -- 'eval' *)
 
-val use_strings =
+fun use_text txt =
   let
-    fun exec line =
-      let
-        val is_first = ref true;
-
-        fun get_line () =
-          if ! is_first then (is_first := false; line)
-          else raise Io "use_strings: buffer exhausted";
-      in
-        PolyML.compiler (get_line, print) ()
-      end;
-
-    fun execs [] = ()
-      | execs (line :: lines) = (exec line; execs lines);
-  in execs end;
+    val buffer = ref (explode txt);
+    fun get () =
+      (case ! buffer of
+        [] => ""
+      | c :: cs => (buffer := cs; c));
+    fun exec () =
+      (case ! buffer of
+        [] => ()
+      | _ => (PolyML.compiler (get, print) (); exec ()));
+  in exec () end;
 
 
 
diff -r 224887671646 -r 301c37df931d src/Pure/ML-Systems/smlnj-0.93.ML
--- a/src/Pure/ML-Systems/smlnj-0.93.ML	Mon Jun 15 11:05:25 1998 +0200
+++ b/src/Pure/ML-Systems/smlnj-0.93.ML	Mon Jun 15 11:06:00 1998 +0200
@@ -81,8 +81,7 @@
 
 (* ML command execution *)
 
-fun use_strings commands =
-  System.Compile.use_stream (open_string (implode commands));
+val use_text = System.Compile.use_stream o open_string;
 
 
 
diff -r 224887671646 -r 301c37df931d src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Mon Jun 15 11:05:25 1998 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Mon Jun 15 11:06:00 1998 +0200
@@ -82,7 +82,7 @@
 
 (* ML command execution *)
 
-val use_strings = Compiler.Interact.useStream o TextIO.openString o implode;
+val use_text = Compiler.Interact.useStream o TextIO.openString;
 
 
 
diff -r 224887671646 -r 301c37df931d src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Mon Jun 15 11:05:25 1998 +0200
+++ b/src/Pure/Thy/thm_database.ML	Mon Jun 15 11:06:00 1998 +0200
@@ -52,7 +52,7 @@
   let val thm' = store_thm (name, thm) in
     if is_ml_identifier name then
       (qed_thm := Some thm';
-        use_strings ["val " ^ name ^ " = the (! ThmDatabase.qed_thm);"])
+        use_text ("val " ^ name ^ " = the (! ThmDatabase.qed_thm);"))
     else warning ("Cannot bind thm " ^ quote name ^ " as ML value")
   end;
 
diff -r 224887671646 -r 301c37df931d src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Mon Jun 15 11:05:25 1998 +0200
+++ b/src/Pure/Thy/thy_read.ML	Mon Jun 15 11:06:00 1998 +0200
@@ -267,7 +267,7 @@
              Use.use ml_file);
 
        (*Store theory again because it could have been redefined*)
-       use_strings ["val _ = store_theory " ^ tname ^ ".thy;"];
+       use_text ("val _ = store_theory " ^ tname ^ ".thy;");
 
        (*Add theory to list of all loaded theories (for index.html)
          and add it to its parents' sub-charts*)