src/Pure/Concurrent/future.ML
changeset 32229 abdc0f6214c8
parent 32228 7622c03141b0
child 32230 9f6461b1c9cc
     1.1 --- a/src/Pure/Concurrent/future.ML	Mon Jul 27 16:53:28 2009 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Mon Jul 27 17:12:19 2009 +0200
     1.3 @@ -124,10 +124,11 @@
     1.4  fun SYNCHRONIZED name = SimpleThread.synchronized name lock;
     1.5  
     1.6  fun wait cond = (*requires SYNCHRONIZED*)
     1.7 -  ConditionVar.wait (cond, lock);
     1.8 +  ConditionVar.wait (cond, lock) handle Exn.Interrupt => ();
     1.9  
    1.10 -fun wait_timeout cond timeout = (*requires SYNCHRONIZED*)
    1.11 -  ignore (ConditionVar.waitUntil (cond, lock, Time.+ (Time.now (), timeout)));
    1.12 +fun wait_interruptible cond timeout = (*requires SYNCHRONIZED*)
    1.13 +  interruptible (fn () =>
    1.14 +    ignore (ConditionVar.waitUntil (cond, lock, Time.+ (Time.now (), timeout)))) ();
    1.15  
    1.16  fun signal cond = (*requires SYNCHRONIZED*)
    1.17    ConditionVar.signal cond;
    1.18 @@ -280,7 +281,7 @@
    1.19      (*delay loop*)
    1.20      val delay =
    1.21        Time.fromMilliseconds (if not (! do_shutdown) andalso null (! canceled) then 500 else 50);
    1.22 -    val _ = interruptible (fn () => wait_timeout scheduler_event delay) ()
    1.23 +    val _ = wait_interruptible scheduler_event delay
    1.24        handle Exn.Interrupt => List.app do_cancel (Task_Queue.cancel_all (! queue));
    1.25  
    1.26      (*shutdown*)