diff -r b8db43faaf9e -r 288a504c24d6 src/Pure/ML-Systems/polyml-interrupt-timeout.ML
--- a/src/Pure/ML-Systems/polyml-interrupt-timeout.ML	Thu Nov 09 11:58:51 2006 +0100
+++ b/src/Pure/ML-Systems/polyml-interrupt-timeout.ML	Thu Nov 09 16:14:43 2006 +0100
@@ -1,47 +1,26 @@
 (*  Title:      Pure/ML-Systems/polyml-interrupt-timeout.ML
     ID:         $Id$
-    Author:     Tjark Weber, Makarius
+    Author:     Tjark Weber
     Copyright   2006
 
 Bounded time execution (similar to SML/NJ's TimeLimit structure) for Poly/ML.
 *)
 
-(* FIXME: this code appears to disable signal handling in child databases altogether (?)
-local
-
-  val alarm_active = ref false;
-
-  val _ = Signal.signal (Posix.Signal.alrm, Signal.SIG_HANDLE (fn _ =>
-    let val active = ! alarm_active in
-      alarm_active := false;
-      if active then
-        Process.interruptConsoleProcesses ()
-      else
-        ()
-    end));
-
-in
+(* Note: This code may cause an infrequent segmentation fault (due to a race
+         condition between process creation/termination and garbage collection)
+         before PolyML 5.0. *)
 
-  fun interrupt_timeout time f x =
-  let
-    fun deactivate_alarm () = (
-      alarm_active := false;
-      Posix.Process.alarm Time.zeroTime
-    )
-  in
-    alarm_active := true;
-    Posix.Process.alarm time;
-    let val result = f x in
-      deactivate_alarm ();
-      result
-    end handle exn => (
-      deactivate_alarm ();
-      raise exn
-    )
-  end;
-
-end;
-*)
+(* Note: f must not manipulate the timer used by Posix.Process.sleep *)
 
 fun interrupt_timeout time f x =
-  f x;
+let
+  val ch = Process.channel ()
+  val interrupt_timer = Process.console (fn () =>
+    (Posix.Process.sleep time; Process.send (ch, NONE)))
+  val interrupt_worker = Process.console (fn () =>
+    Process.send (ch, SOME (capture f x)))
+in
+  case Process.receive ch of
+    NONE    => (interrupt_worker (); raise Interrupt)
+  | SOME fx => (interrupt_timer (); release fx)
+end;