# HG changeset patch
# User clasohm
# Date 769952271 -7200
# Node ID 18c9c28d0f7e506eaa88719640febdd8673f4f5d
# Parent  712dceb1ecc790346f99af846dcbd1a2cc3f7b73
changed use_string's type to string list -> unit because POLY can only
handle one command per string

diff -r 712dceb1ecc7 -r 18c9c28d0f7e src/Pure/NJ.ML
--- a/src/Pure/NJ.ML	Thu May 26 12:55:52 1994 +0200
+++ b/src/Pure/NJ.ML	Thu May 26 13:37:51 1994 +0200
@@ -98,5 +98,6 @@
 
 (*** ML command execution ***)
 
-fun use_string commands = System.Compile.use_stream (open_string commands);
+fun use_string commands = 
+  System.Compile.use_stream (open_string (implode commands));
 
diff -r 712dceb1ecc7 -r 18c9c28d0f7e src/Pure/POLY.ML
--- a/src/Pure/POLY.ML	Thu May 26 12:55:52 1994 +0200
+++ b/src/Pure/POLY.ML	Thu May 26 13:37:51 1994 +0200
@@ -50,6 +50,11 @@
 
 fun apr (f,y) x = f(x,y);
 
+fun seq (proc: 'a -> unit) : 'a list -> unit =
+  let fun seqf [] = ()
+        | seqf (x :: xs) = (proc x; seqf xs)
+  in seqf end;
+
 in
 
 (*Get a string containing the time of last modification, attributes, owner
@@ -83,15 +88,18 @@
      implode path
   end;
 
-end;
-
 
 (*** ML command execution ***)
 
-fun use_string commands =
-  let val firstLine = ref true;
-      fun getLine () =
-        if !firstLine
-        then (firstLine := false; commands ^ ";\n")
-        else raise Io "execML: buffer exhausted"
-  in PolyML.compiler (getLine, fn s => output (std_out, s)) () end;
+val use_string =
+  let fun exec command =
+    let val firstLine = ref true;
+
+        fun getLine () =
+          if !firstLine
+          then (firstLine := false; command)
+          else raise Io "use_string: buffer exhausted"
+    in PolyML.compiler (getLine, fn s => output (std_out, s)) () end
+  in seq exec end;
+
+end;