# HG changeset patch
# User wenzelm
# Date 1262798563 -3600
# Node ID eedea6f0b37ebca9ebbea09b9f41961c1271fd9e
# Parent  16bf3e9786a35434370c9bbbe74761682a1a50a9
more robust cancelation, notably of passive futures without scheduler running;

diff -r 16bf3e9786a3 -r eedea6f0b37e src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Wed Jan 06 18:14:16 2010 +0100
+++ b/src/Pure/Concurrent/future.ML	Wed Jan 06 18:22:43 2010 +0100
@@ -505,7 +505,8 @@
   else interruptible f x;
 
 (*cancel: present and future group members will be interrupted eventually*)
-fun cancel_group group = SYNCHRONIZED "cancel" (fn () => cancel_later group);
+fun cancel_group group =
+  SYNCHRONIZED "cancel" (fn () => if cancel_now group then () else cancel_later group);
 fun cancel x = cancel_group (group_of x);