# HG changeset patch
# User wenzelm
# Date 1204831070 -3600
# Node ID d34b68c21f9a8e3c74236ad349ac57667d644dea
# Parent  2d026932f7105793b3fc70e09229ff26fc799fcf
common setup for system_out/system;

diff -r 2d026932f710 -r d34b68c21f9a src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Thu Mar 06 20:17:49 2008 +0100
+++ b/src/Pure/General/file.ML	Thu Mar 06 20:17:50 2008 +0100
@@ -98,8 +98,10 @@
       (case getenv "ISABELLE_FILE_IDENT" of
         "" => Path.implode (full_path path) ^ ": " ^ Time.toString time
       | cmd =>
-         let val id = execute ("\"$ISABELLE_HOME/lib/scripts/fileident\" " ^ shell_path path) in
-           if id <> "" then id
+         let
+           val (id, rc) = system_out ("\"$ISABELLE_HOME/lib/scripts/fileident\" " ^ shell_path path)
+         in
+           if id <> "" andalso rc = 0 then id
            else error ("Failed to identify file " ^ quote (Path.implode path) ^ " by " ^ cmd)
          end)));
 
diff -r 2d026932f710 -r d34b68c21f9a src/Pure/General/secure.ML
--- a/src/Pure/General/secure.ML	Thu Mar 06 20:17:49 2008 +0100
+++ b/src/Pure/General/secure.ML	Thu Mar 06 20:17:50 2008 +0100
@@ -14,7 +14,7 @@
   val use_file: (string -> unit) * (string -> 'a) -> bool -> string -> unit
   val use: string -> unit
   val commit: unit -> unit
-  val execute: string -> string
+  val system_out: string -> string * int
   val system: string -> int
 end;
 
@@ -57,11 +57,10 @@
 
 fun secure_shell () = deny_secure "Cannot execute shell commands in secure mode";
 
-val orig_execute = execute;
-val orig_system = system;
+val orig_system_out = system_out;
 
-fun execute s = (secure_shell (); orig_execute s);
-fun system s = (secure_shell (); orig_system s);
+fun system_out s = (secure_shell (); orig_system_out s);
+fun system s = #2 (system_out s);
 
 end;
 
@@ -69,5 +68,5 @@
 val use_text = Secure.use_text;
 val use_file = Secure.use_file;
 fun use s = Secure.use s handle ERROR msg => (writeln msg; raise Fail "ML error");
-val execute = Secure.execute;
+val system_out = Secure.system_out;
 val system = Secure.system;
diff -r 2d026932f710 -r d34b68c21f9a src/Pure/ML-Systems/alice.ML
--- a/src/Pure/ML-Systems/alice.ML	Thu Mar 06 20:17:49 2008 +0100
+++ b/src/Pure/ML-Systems/alice.ML	Thu Mar 06 20:17:50 2008 +0100
@@ -11,6 +11,7 @@
 - use "ML-Systems/exn.ML";
 - use "ML-Systems/multithreading.ML";
 - use "ML-Systems/time_limit.ML";
+- use "ML-Systems/system_shell.ML";
 - use "ML-Systems/alice.ML";
 - use "ROOT.ML";
 - Session.finish ();
@@ -143,29 +144,9 @@
 
 (** OS related **)
 
-(* current directory *)
-
 val cd = OS.FileSys.chDir;
 val pwd = OS.FileSys.getDir;
 
-
-(* 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 = OS.Process.system: string -> int;
 
 structure OS =
@@ -182,9 +163,6 @@
   end;
 end;
 
-
-(* getenv *)
-
 fun getenv var =
   (case OS.Process.getEnv var of
     NONE => ""
diff -r 2d026932f710 -r d34b68c21f9a src/Pure/ML-Systems/mosml.ML
--- a/src/Pure/ML-Systems/mosml.ML	Thu Mar 06 20:17:49 2008 +0100
+++ b/src/Pure/ML-Systems/mosml.ML	Thu Mar 06 20:17:50 2008 +0100
@@ -38,6 +38,7 @@
 use "ML-Systems/universal.ML";
 use "ML-Systems/multithreading.ML";
 use "ML-Systems/time_limit.ML";
+use "ML-Systems/system_shell.ML";
 
 
 (*low-level pointer equality*)
@@ -178,38 +179,11 @@
 
 (** OS related **)
 
-(* current directory *)
-
 val cd = OS.FileSys.chDir;
 val pwd = OS.FileSys.getDir;
 
-
-(* 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 = FileSys.tmpName ();
-    val is = (Process.system (command ^ " > " ^ tmp_name); TextIO.openIn tmp_name);
-    val result = TextIO.inputAll is;
-  in
-    TextIO.closeIn is;
-    FileSys.remove tmp_name;
-    result
-  end;
-
-(*plain version; with return code*)
-fun system cmd =
-  if Process.system cmd = Process.success then 0 else 1;
-
-
 val string_of_pid = Int.toString;
 
-
-(* getenv *)
-
 fun getenv var =
   (case Process.getEnv var of
     NONE => ""
diff -r 2d026932f710 -r d34b68c21f9a src/Pure/ML-Systems/polyml_common.ML
--- a/src/Pure/ML-Systems/polyml_common.ML	Thu Mar 06 20:17:49 2008 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML	Thu Mar 06 20:17:50 2008 +0100
@@ -9,6 +9,8 @@
 else use "ML-Systems/universal.ML";
 use "ML-Systems/multithreading.ML";
 use "ML-Systems/time_limit.ML";
+use "ML-Systems/system_shell.ML";
+
 
 
 (** ML system and platform related **)
@@ -190,27 +192,6 @@
 val pwd = OS.FileSys.getDir;
 
 
-(* 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*)
-fun system cmd =
-  if OS.Process.isSuccess (OS.Process.system cmd) then 0 else 1;
-
-
 (*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));
diff -r 2d026932f710 -r d34b68c21f9a src/Pure/ML-Systems/smlnj.ML
--- 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 *)
diff -r 2d026932f710 -r d34b68c21f9a src/Pure/ML-Systems/system_shell.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/system_shell.ML	Thu Mar 06 20:17:50 2008 +0100
@@ -0,0 +1,44 @@
+(*  Title:      Pure/ML-Systems/system_shell.ML
+    ID:         $Id$
+    Author:     Makarius
+
+Generic system shell processes (no provisions to propagate interrupts;
+might still work via the controlling tty).
+*)
+
+local
+
+fun read_file name =
+  let val is = TextIO.openIn name
+  in TextIO.inputAll is before TextIO.closeIn is end;
+
+fun write_file name txt =
+  let val os = TextIO.openOut name
+  in TextIO.output (os, txt) before TextIO.closeOut os end;
+
+in
+
+fun system_out script =
+  let
+    val script_name = OS.FileSys.tmpName ();
+    val _ = write_file script_name script;
+
+    val output_name = OS.FileSys.tmpName ();
+
+    val status =
+      OS.Process.system ("perl -w \"$ISABELLE_HOME/lib/scripts/system.pl\" nogroup " ^
+        script_name ^ " /dev/null " ^ output_name);
+    val rc =
+      (case Posix.Process.fromStatus status of
+        Posix.Process.W_EXITED => 0
+      | Posix.Process.W_EXITSTATUS w => Word8.toInt w
+      | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
+      | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
+
+    val output = read_file output_name handle IO.Io _ => "";
+    val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
+    val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
+  in (output, rc) end;
+
+end;
+