src/Pure/ML-Systems/smlnj.ML
changeset 26220 d34b68c21f9a
parent 26084 a7475459c740
child 26385 ae7564661e76
--- a/src/Pure/ML-Systems/smlnj.ML	Thu Mar 06 20:17:49 2008 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Thu Mar 06 20:17:50 2008 +0100
@@ -9,6 +9,7 @@
 use "ML-Systems/exn.ML";
 use "ML-Systems/universal.ML";
 use "ML-Systems/multithreading.ML";
+use "ML-Systems/system_shell.ML";
 
 
 (*low-level pointer equality*)
@@ -229,27 +230,12 @@
 
 (* system command execution *)
 
-(*execute Unix command which doesn't take any input from stdin and
-  sends its output to stdout; could be done more easily by Unix.execute,
-  but that function doesn't use the PATH*)
-fun execute command =
-  let
-    val tmp_name = OS.FileSys.tmpName ();
-    val is = (OS.Process.system (command ^ " > " ^ tmp_name); TextIO.openIn tmp_name);
-    val result = TextIO.inputAll is;
-  in
-    TextIO.closeIn is;
-    OS.FileSys.remove tmp_name;
-    result
-  end;
-
-(*plain version; with return code*)
-val system = mk_int o OS.Process.system;
+val system_out = (fn (output, rc) => (output, mk_int rc)) o system_out;
 
 
 (*Convert a process ID to a decimal string (chiefly for tracing)*)
 fun string_of_pid pid =
-    Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord pid));
+  Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord pid));
 
 
 (* getenv *)