always signal after cancel_group: passive tasks may have become active;
authorwenzelm
Wed Apr 11 12:15:56 2012 +0200 (2012-04-11)
changeset 474219624408d8827
parent 47420 0dbe6c69eda2
child 47422 5832630f049a
always signal after cancel_group: passive tasks may have become active;
src/Pure/Concurrent/future.ML
     1.1 --- a/src/Pure/Concurrent/future.ML	Wed Apr 11 11:44:21 2012 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Wed Apr 11 12:15:56 2012 +0200
     1.3 @@ -411,10 +411,9 @@
     1.4  
     1.5  fun cancel_group group = SYNCHRONIZED "cancel_group" (fn () =>
     1.6    let
     1.7 -    val running = cancel_now group;
     1.8 -    val _ =
     1.9 -      if null running then ()
    1.10 -      else (cancel_later group; signal work_available; scheduler_check ());
    1.11 +    val _ = if null (cancel_now group) then () else cancel_later group;
    1.12 +    val _ = signal work_available;
    1.13 +    val _ = scheduler_check ();
    1.14    in () end);
    1.15  
    1.16  fun cancel x = cancel_group (Task_Queue.group_of_task (task_of x));