cancel, shutdown: notify_all;

--- 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")));