--- 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;