# HG changeset patch
# User clasohm
# Date 769347950 -7200
# Node ID 85ff48546a05a47722903f90c274793c6f442f72
# Parent  ab8917806779bfa17a9a809a9567c5a757c864ea
added use_string: string -> unit to execute ML commands passed in a string

diff -r ab8917806779 -r 85ff48546a05 src/Pure/NJ.ML
--- 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);
+
diff -r ab8917806779 -r 85ff48546a05 src/Pure/POLY.ML
--- 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;