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