# HG changeset patch
# User wenzelm
# Date 1231602792 -3600
# Node ID 0ebe652bfd5ab212b011799f4fa7d09dc33335d1
# Parent  018d5c88c7a8d3bbad4241e37a258bd5f17bec45
added cancel_group;

diff -r 018d5c88c7a8 -r 0ebe652bfd5a src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Sat Jan 10 16:00:34 2009 +0100
+++ b/src/Pure/Concurrent/future.ML	Sat Jan 10 16:53:12 2009 +0100
@@ -45,6 +45,7 @@
   val join: 'a future -> 'a
   val map: ('a -> 'b) -> 'a future -> 'b future
   val interrupt_task: string -> unit
+  val cancel_group: group -> unit
   val cancel: 'a future -> unit
   val shutdown: unit -> unit
 end;
@@ -330,17 +331,18 @@
   end;
 
 
-(* cancel *)
+(* cancellation *)
 
 (*interrupt: permissive signal, may get ignored*)
 fun interrupt_task id = SYNCHRONIZED "interrupt"
   (fn () => Task_Queue.interrupt_external (! queue) id);
 
 (*cancel: present and future group members will be interrupted eventually*)
-fun cancel x =
+fun cancel_group group =
  (scheduler_check "cancel check";
-  SYNCHRONIZED "cancel" (fn () => (do_cancel (group_of x); notify_all ())));
+  SYNCHRONIZED "cancel" (fn () => (do_cancel group; notify_all ())));
 
+fun cancel x = cancel_group (group_of x);
 
 
 (** global join and shutdown **)