# HG changeset patch
# User wenzelm
# Date 1221164579 -7200
# Node ID 3a8b3453129a15392d033403245b5243fd8a33c1
# Parent  e2431cc4dc66261b63fcbbba091b3059aa8bed32
cancel, shutdown: notify_all;

diff -r e2431cc4dc66 -r 3a8b3453129a src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Thu Sep 11 22:22:20 2008 +0200
+++ b/src/Pure/Concurrent/future.ML	Thu Sep 11 22:22:59 2008 +0200
@@ -277,7 +277,8 @@
 
 (*cancel: present and future group members will be interrupted eventually*)
 fun cancel x =
- (scheduler_check (); SYNCHRONIZED "cancel" (fn () => change canceled (cons (group_of x))));
+ (scheduler_check ();
+  SYNCHRONIZED "cancel" (fn () => (change canceled (cons (group_of x)); notify_all ())));
 
 
 (*global join and shutdown*)
@@ -287,6 +288,7 @@
    (while not (scheduler_active ()) do wait "shutdown: scheduler inactive";
     while not (TaskQueue.is_empty (! queue)) do wait "shutdown: join";
     do_shutdown := true;
+    notify_all ();
     while not (null (! workers)) do wait "shutdown: workers";
     while scheduler_active () do wait "shutdown: scheduler still active")));