more robust TimeLimit: make double sure that watchdog has terminated and interrupts received during uninterruptible state are propagated (NB: Thread.testInterrupt requires InterruptSynch in Poly/ML 5.4.0 or earlier);

--- a/src/Pure/Concurrent/time_limit.ML	Sat Feb 05 20:38:32 2011 +0100
+++ b/src/Pure/Concurrent/time_limit.ML	Mon Feb 07 23:57:03 2011 +0100
@@ -1,7 +1,7 @@
 (*  Title:      Pure/Concurrent/time_limit.ML
     Author:     Makarius
 
-Execution with time limit.
+Execution with time limit (considerable overhead due to fork of watchdog thread).
 *)
 
 signature TIME_LIMIT =
@@ -15,18 +15,29 @@
 
 exception TimeOut;
 
-fun timeLimit time f x = uninterruptible (fn restore_attributes => fn () =>
-  let
-    val worker = Thread.self ();
-    val timeout = Unsynchronized.ref false;
-    val watchdog = Thread.fork (fn () =>
-      (OS.Process.sleep time; timeout := true; Thread.interrupt worker), []);
+fun timeLimit time f x =
+  Multithreading.with_attributes Multithreading.no_interrupts (fn orig_atts =>
+    let
+      val main = Thread.self ();
+      val timeout = Unsynchronized.ref false;
+      val watchdog = Simple_Thread.fork true (fn () =>
+        (OS.Process.sleep time; timeout := true; Thread.interrupt main));
+
+      val result = Exn.capture (fn () => Multithreading.with_attributes orig_atts (fn _ => f x)) ();
 
-    val result = Exn.capture (restore_attributes f) x;
-    val was_timeout = Exn.is_interrupt_exn result andalso ! timeout;
+      val _ = Thread.interrupt watchdog handle Thread _ => ();
+      val _ = while Thread.isActive watchdog do OS.Process.sleep (seconds 0.0001);
 
-    val _ = Thread.interrupt watchdog handle Thread _ => ();
-  in if was_timeout then raise TimeOut else Exn.release result end) ();
+      val test =
+        Exn.capture (fn () =>
+          Multithreading.with_attributes (Multithreading.sync_interrupts orig_atts)
+            (fn _ => Thread.testInterrupt ())) ();
+    in
+      if ! timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test)
+      then raise TimeOut
+      else if Exn.is_interrupt_exn test then Exn.interrupt ()
+      else Exn.release result
+    end);
 
 end;