--- a/src/Pure/ML-Systems/mlworks.ML Wed Oct 13 19:42:12 1999 +0200
+++ b/src/Pure/ML-Systems/mlworks.ML Wed Oct 13 19:42:46 1999 +0200
@@ -78,7 +78,7 @@
(* ML command execution *)
(*Can one redirect 'use' directly to an instream?*)
-fun use_text _ txt =
+fun use_text _ _ txt =
let
val tmp_name = OS.FileSys.tmpName ();
val tmp_file = TextIO.openOut tmp_name;
@@ -121,6 +121,10 @@
result
end;
+(*plain version; with return code*)
+fun system cmd =
+ if OS.Process.system cmd = OS.Process.success then 0 else 1;
+
(* file handling *)
--- a/src/Pure/ML-Systems/polyml.ML Wed Oct 13 19:42:12 1999 +0200
+++ b/src/Pure/ML-Systems/polyml.ML Wed Oct 13 19:42:46 1999 +0200
@@ -49,7 +49,7 @@
(* ML command execution -- 'eval' *)
-fun use_text verbose txt =
+fun use_text print verbose txt =
let
val in_buffer = ref (explode txt);
val out_buffer = ref ([]: string list);
@@ -101,12 +101,11 @@
fun execute command =
let
val (is, os) = ExtendedIO.execute command;
+ val _ = close_out os;
val result = input (is, 999999);
- in
- close_out os;
- close_in is;
- result
- end;
+ in close_in is; result end;
+
+fun system cmd = (print (execute cmd); 0); (* FIXME rc not available *)
(* file handling *)
--- a/src/Pure/ML-Systems/smlnj-0.93.ML Wed Oct 13 19:42:12 1999 +0200
+++ b/src/Pure/ML-Systems/smlnj-0.93.ML Wed Oct 13 19:42:46 1999 +0200
@@ -90,7 +90,7 @@
(* ML command execution *)
-fun use_text _ = System.Compile.use_stream o open_string;
+fun use_text _ _ = System.Compile.use_stream o open_string;
@@ -180,6 +180,9 @@
result
end;
+(*plain version; with return code*)
+fun system cmd = System.system cmd div 256;
+
(* file handling *)
--- a/src/Pure/ML-Systems/smlnj.ML Wed Oct 13 19:42:12 1999 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML Wed Oct 13 19:42:46 1999 +0200
@@ -80,7 +80,7 @@
(* ML command execution *)
-fun use_text verbose txt =
+fun use_text print verbose txt =
let
val ref out_orig = Compiler.Control.Print.out;
@@ -189,6 +189,9 @@
result
end;
+(*plain version; with return code*)
+val system = OS.Process.system: string -> int;
+
(* file handling *)