added use_string: string -> unit to execute ML commands passed in a string

--- a/src/Pure/NJ.ML	Thu May 19 13:13:27 1994 +0200
+++ b/src/Pure/NJ.ML	Thu May 19 13:45:50 1994 +0200
@@ -94,3 +94,9 @@
 
 (*Get pathname of current working directory *)
 fun pwd () = System.Directory.getWD ();
+
+
+(*** ML command execution ***)
+
+fun use_string commands = System.Compile.use_stream (open_string commands);
+

--- a/src/Pure/POLY.ML	Thu May 19 13:13:27 1994 +0200
+++ b/src/Pure/POLY.ML	Thu May 19 13:45:50 1994 +0200
@@ -85,3 +85,13 @@
 
 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;