always signal after cancel_group: passive tasks may have become active;
authorwenzelm
Wed, 11 Apr 2012 12:15:56 +0200
changeset 47421 9624408d8827
parent 47420 0dbe6c69eda2
child 47422 5832630f049a
always signal after cancel_group: passive tasks may have become active;
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));