src/Pure/ML-Systems/polyml.ML
changeset 7855 092a6435afad
parent 7148 e9c253036b45
child 7890 0aa16bc2abdb
--- 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 *)