# HG changeset patch
# User wenzelm
# Date 1334139356 -7200
# Node ID 9624408d88271b267ee3c4bbcd0a3497e564a761
# Parent  0dbe6c69eda2d4edbe1e398108ad258b65d9255d
always signal after cancel_group: passive tasks may have become active;

diff -r 0dbe6c69eda2 -r 9624408d8827 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Wed Apr 11 11:44:21 2012 +0200
+++ b/src/Pure/Concurrent/future.ML	Wed Apr 11 12:15:56 2012 +0200
@@ -411,10 +411,9 @@
 
 fun cancel_group group = SYNCHRONIZED "cancel_group" (fn () =>
   let
-    val running = cancel_now group;
-    val _ =
-      if null running then ()
-      else (cancel_later group; signal work_available; scheduler_check ());
+    val _ = if null (cancel_now group) then () else cancel_later group;
+    val _ = signal work_available;
+    val _ = scheduler_check ();
   in () end);
 
 fun cancel x = cancel_group (Task_Queue.group_of_task (task_of x));