# HG changeset patch
# User wenzelm
# Date 1368826262 -7200
# Node ID 4b4ff1d3b723a62a04aaf2eae06b28d8febc8851
# Parent  fd533ac64390538eca1d950069a44de21fb792b6
back to more paranoid interrupt test after request is cancelled -- avoid race condition;

diff -r fd533ac64390 -r 4b4ff1d3b723 src/Pure/Concurrent/time_limit.ML
--- a/src/Pure/Concurrent/time_limit.ML	Fri May 17 21:15:33 2013 +0200
+++ b/src/Pure/Concurrent/time_limit.ML	Fri May 17 23:31:02 2013 +0200
@@ -28,9 +28,11 @@
         Exn.capture (fn () => Multithreading.with_attributes orig_atts (fn _ => f x)) ();
 
       val was_timeout = not (Event_Timer.cancel request);
+      val test = Exn.capture Multithreading.interrupted ();
     in
-      if was_timeout andalso Exn.is_interrupt_exn result
+      if was_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);