added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);

--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Feb 19 20:34:29 2008 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Feb 19 20:34:30 2008 +0100
@@ -11,6 +11,7 @@
 sig
   val interruptible: ('a -> 'b) -> 'a -> 'b
   val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
+  val system_out: string -> string * int
   structure TimeLimit: TIME_LIMIT
 end;
 
@@ -58,6 +59,14 @@
 fun show "" = "" | show name = " " ^ name;
 fun show' "" = "" | show' name = " [" ^ name ^ "]";
 
+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;
+
 
 (* thread attributes *)
 
@@ -111,6 +120,70 @@
 end;
 
 
+(* system shell processes, with propagation of interrupts *)
+
+fun system_out script = uninterruptible (fn restore_attributes => fn () =>
+  let
+    val script_name = OS.FileSys.tmpName ();
+    val _ = write_file script_name script;
+
+    val pid_name = OS.FileSys.tmpName ();
+    val output_name = OS.FileSys.tmpName ();
+
+    (*result state*)
+    datatype result = Wait | Signal | Result of int;
+    val result = ref Wait;
+    val result_mutex = Mutex.mutex ();
+    val result_cond = ConditionVar.conditionVar ();
+    fun set_result res =
+      (Mutex.lock result_mutex; result := res; Mutex.unlock result_mutex;
+        ConditionVar.signal result_cond);
+
+    val _ = Mutex.lock result_mutex;
+
+    (*system thread*)
+    val system_thread = Thread.fork (fn () =>
+      let
+        val status =
+          OS.Process.system ("perl -w \"$ISABELLE_HOME/lib/scripts/system.pl\" group " ^
+            script_name ^ " " ^ pid_name ^ " " ^ output_name);
+        val res =
+          (case Posix.Process.fromStatus status of
+            Posix.Process.W_EXITED => Result 0
+          | Posix.Process.W_EXITSTATUS 0wx82 => Signal
+          | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w)
+          | Posix.Process.W_SIGNALED s =>
+              if s = Posix.Signal.int then Signal
+              else Result (256 + LargeWord.toInt (Posix.Signal.toWord s))
+          | Posix.Process.W_STOPPED s => Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
+      in set_result res end handle _ => set_result (Result 2), []);
+
+    (*main thread -- proxy for interrupts*)
+    fun kill n =
+      (case Int.fromString (read_file pid_name) of
+        SOME pid =>
+          Posix.Process.kill
+            (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)),
+              Posix.Signal.int)
+      | NONE => ())
+      handle OS.SysErr _ => () | IO.Io _ =>
+        (OS.Process.sleep (Time.fromMilliseconds 100); if n > 0 then kill (n - 1) else ());
+
+    val _ = while ! result = Wait do
+      restore_attributes (fn () =>
+        (ConditionVar.waitUntil (result_cond, result_mutex, Time.now () + Time.fromMilliseconds 100); ())
+          handle Interrupt => kill 10) ();
+
+    (*cleanup*)
+    val output = read_file output_name handle IO.Io _ => "";
+    val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
+    val _ = OS.FileSys.remove pid_name handle OS.SysErr _ => ();
+    val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
+    val _ = Thread.interrupt system_thread handle Thread _ => ();
+    val rc = (case ! result of Signal => raise Interrupt | Result rc => rc);
+  in (output, rc) end) ();
+
+
 (* critical section -- may be nested within the same thread *)
 
 local