src/Pure/ML-Systems/multithreading_polyml.ML

--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Nov 27 16:27:52 2010 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Nov 27 16:29:53 2010 +0100
@@ -8,7 +8,6 @@
 sig
   val interruptible: ('a -> 'b) -> 'a -> 'b
   val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
-  val bash_output: string -> string * int
   structure TimeLimit: TIME_LIMIT
 end;
 
@@ -42,20 +41,6 @@
 fun enabled () = max_threads_value () > 1;
 
 
-(* misc utils *)
-
-fun show "" = "" | show name = " " ^ name;
-fun show' "" = "" | show' name = " [" ^ name ^ "]";
-
-fun read_file name =
-  let val is = TextIO.openIn name
-  in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
-
-fun write_file name txt =
-  let val os = TextIO.openOut name
-  in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
-
-
 (* thread attributes *)
 
 val no_interrupts =
@@ -156,71 +141,6 @@
 end;
 
 
-(* GNU bash processes, with propagation of interrupts *)
-
-fun bash_output script = with_attributes no_interrupts (fn orig_atts =>
-  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 lock = Mutex.mutex ();
-    val cond = ConditionVar.conditionVar ();
-    fun set_result res =
-      (Mutex.lock lock; result := res; ConditionVar.signal cond; Mutex.unlock lock);
-
-    val _ = Mutex.lock lock;
-
-    (*system thread*)
-    val system_thread = Thread.fork (fn () =>
-      let
-        val status =
-          OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^ pid_name ^
-            " script \"exec bash " ^ script_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 _ (*sic*) => 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 (seconds 0.1); if n > 0 then kill (n - 1) else ());
-
-    val _ =
-      while ! result = Wait do
-        let val res =
-          sync_wait (SOME orig_atts)
-            (SOME (Time.+ (Time.now (), seconds 0.1))) cond lock
-        in if Exn.is_interrupt_exn res then kill 10 else () end;
-
-    (*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 => Exn.interrupt () | Result rc => rc);
-  in (output, rc) end);
-
-
 (* critical section -- may be nested within the same thread *)
 
 local
@@ -229,6 +149,9 @@
 val critical_thread = ref (NONE: Thread.thread option);
 val critical_name = ref "";
 
+fun show "" = "" | show name = " " ^ name;
+fun show' "" = "" | show' name = " [" ^ name ^ "]";
+
 in
 
 fun self_critical () =