1.1 --- a/src/Pure/Concurrent/future.ML	Mon Jul 27 15:06:33 2009 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Mon Jul 27 15:30:21 2009 +0200
     1.3 @@ -135,6 +135,11 @@
     1.4  fun broadcast cond = (*requires SYNCHRONIZED*)
     1.5    ConditionVar.broadcast cond;
     1.6  
     1.7 +fun broadcast_all () = (*requires SYNCHRONIZED*)
     1.8 + (ConditionVar.broadcast scheduler_event;
     1.9 +  ConditionVar.broadcast work_available;
    1.10 +  ConditionVar.broadcast work_finished);
    1.11 +
    1.12  end;
    1.13  
    1.14  
    1.15 @@ -179,7 +184,7 @@
    1.16    in (result, job) end;
    1.17  
    1.18  fun do_cancel group = (*requires SYNCHRONIZED*)
    1.19 -  change canceled (insert Task_Queue.eq_group group);
    1.20 + (change canceled (insert Task_Queue.eq_group group); broadcast scheduler_event);
    1.21  
    1.22  fun execute name (task, group, jobs) =
    1.23    let
    1.24 @@ -263,7 +268,9 @@
    1.25        else ();
    1.26  
    1.27      (*canceled groups*)
    1.28 -    val _ = change canceled (filter_out (Task_Queue.cancel (! queue)));
    1.29 +    val _ =
    1.30 +      if null (! canceled) then ()
    1.31 +      else (change canceled (filter_out (Task_Queue.cancel (! queue))); broadcast_all ());
    1.32  
    1.33      val timeout =
    1.34        Time.fromMilliseconds (if not (! do_shutdown) andalso null (! canceled) then 500 else 50);
    1.35 @@ -401,7 +408,7 @@
    1.36  (*cancel_group: present and future group members will be interrupted eventually*)
    1.37  fun cancel_group group =
    1.38   (scheduler_check "cancel check";
    1.39 -  SYNCHRONIZED "cancel" (fn () => (do_cancel group; broadcast scheduler_event)));
    1.40 +  SYNCHRONIZED "cancel" (fn () => do_cancel group));
    1.41  
    1.42  fun cancel x = cancel_group (group_of x);
    1.43  
    1.44 @@ -415,10 +422,7 @@
    1.45       (while not (scheduler_active ()) do wait scheduler_event;
    1.46        while not (Task_Queue.is_empty (! queue)) do wait scheduler_event;
    1.47        do_shutdown := true;
    1.48 -      while scheduler_active () do
    1.49 -       (broadcast work_available;
    1.50 -        broadcast scheduler_event;
    1.51 -        wait scheduler_event))))
    1.52 +      while scheduler_active () do (broadcast_all (); wait scheduler_event))))
    1.53    else ();
    1.54  
    1.55