# HG changeset patch
# User wenzelm
# Date 1248707539 -7200
# Node ID abdc0f6214c87270df76fc1a18af78010c8d5b53
# Parent  7622c03141b053affb6d6f89a9526377cd50dfb4
wait: absorb spurious interrupts;
replaced wait_timeout by explicit wait_interruptible;

diff -r 7622c03141b0 -r abdc0f6214c8 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Mon Jul 27 16:53:28 2009 +0200
+++ b/src/Pure/Concurrent/future.ML	Mon Jul 27 17:12:19 2009 +0200
@@ -124,10 +124,11 @@
 fun SYNCHRONIZED name = SimpleThread.synchronized name lock;
 
 fun wait cond = (*requires SYNCHRONIZED*)
-  ConditionVar.wait (cond, lock);
+  ConditionVar.wait (cond, lock) handle Exn.Interrupt => ();
 
-fun wait_timeout cond timeout = (*requires SYNCHRONIZED*)
-  ignore (ConditionVar.waitUntil (cond, lock, Time.+ (Time.now (), timeout)));
+fun wait_interruptible cond timeout = (*requires SYNCHRONIZED*)
+  interruptible (fn () =>
+    ignore (ConditionVar.waitUntil (cond, lock, Time.+ (Time.now (), timeout)))) ();
 
 fun signal cond = (*requires SYNCHRONIZED*)
   ConditionVar.signal cond;
@@ -280,7 +281,7 @@
     (*delay loop*)
     val delay =
       Time.fromMilliseconds (if not (! do_shutdown) andalso null (! canceled) then 500 else 50);
-    val _ = interruptible (fn () => wait_timeout scheduler_event delay) ()
+    val _ = wait_interruptible scheduler_event delay
       handle Exn.Interrupt => List.app do_cancel (Task_Queue.cancel_all (! queue));
 
     (*shutdown*)