# HG changeset patch
# User clasohm
# Date 814538406 -3600
# Node ID 2edd7a39d92a6a27e7a0a39d24c8bf10fcdc95f1
# Parent  6eb89a693e05774ffba9802aaa344c2c81608568
added "execute"

diff -r 6eb89a693e05 -r 2edd7a39d92a src/Pure/NJ.ML
--- a/src/Pure/NJ.ML	Sun Oct 22 15:16:57 1995 +0100
+++ b/src/Pure/NJ.ML	Tue Oct 24 13:40:06 1995 +0100
@@ -102,3 +102,19 @@
 fun use_string commands = 
   System.Compile.use_stream (open_string (implode commands));
 
+
+(*** System command execution ***)
+
+(*Execute an Unix command which doesn't take any input from stdin and
+  sends its output to stdout.
+  This could be done more easily by IO.execute, but that function
+  seems to be buggy in SML/NJ 0.93.*)
+fun execute command =
+  let val tmp_name = "isa_converted.tmp"
+      val is = (System.system (command ^ " > " ^ tmp_name);
+                open_in tmp_name);
+      val result = input (is, 999999);
+  in close_in is;
+     delete_file tmp_name;
+     result
+  end;
diff -r 6eb89a693e05 -r 2edd7a39d92a src/Pure/POLY.ML
--- a/src/Pure/POLY.ML	Sun Oct 22 15:16:57 1995 +0100
+++ b/src/Pure/POLY.ML	Tue Oct 24 13:40:06 1995 +0100
@@ -103,3 +103,16 @@
   in seq exec end;
 
 end;
+
+
+(*** System command execution ***)
+
+(*Execute an Unix command which doesn't take any input from stdin and
+  sends its output to stdout.*)
+fun execute command =
+  let val (is, os) =  ExtendedIO.execute command;
+      val result = input (is, 999999);
+  in close_out os;
+     close_in is;
+     result
+  end;