--- a/src/Pure/Concurrent/future.ML Mon Jul 27 12:24:27 2009 +0200
+++ b/src/Pure/Concurrent/future.ML Mon Jul 27 13:32:23 2009 +0200
@@ -46,7 +46,6 @@
val join: 'a future -> 'a
val map: ('a -> 'b) -> 'a future -> 'b future
val interruptible_task: ('a -> 'b) -> 'a -> 'b
- val interrupt_task: string -> unit
val cancel_group: group -> unit
val cancel: 'a future -> unit
val shutdown: unit -> unit
@@ -400,11 +399,7 @@
(fn _ => f) x
else interruptible f x;
-(*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*)
+(*cancel_group: present and future group members will be interrupted eventually*)
fun cancel_group group =
(scheduler_check "cancel check";
SYNCHRONIZED "cancel" (fn () => (do_cancel group; broadcast scheduler_event)));