# HG changeset patch
# User wenzelm
# Date 1221082089 -7200
# Node ID 7053c539ecd818850fad3e2c4579535db0bb44e8
# Parent  f019dd2db561a2345136eb5b4ffc622ac2ae50e8
added interrupt_task (external id);
tuned signature;

diff -r f019dd2db561 -r 7053c539ecd8 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Wed Sep 10 23:19:36 2008 +0200
+++ b/src/Pure/Concurrent/future.ML	Wed Sep 10 23:28:09 2008 +0200
@@ -15,9 +15,10 @@
   val shutdown_request: unit -> unit
   val future: group option -> task list -> (unit -> 'a) -> 'a T
   val fork: (unit -> 'a) -> 'a T
-  val cancel: 'a T -> unit
   val join_results: 'a T list -> 'a Exn.result list
   val join: 'a T -> 'a
+  val cancel: 'a T -> unit
+  val interrupt_task: string -> unit
 end;
 
 structure Future: FUTURE =
@@ -251,6 +252,7 @@
 fun cancel x = (scheduler_check (); cancel_request (group_of x));
 
 (*interrupt: adhoc signal, permissive, may get ignored*)
-fun interrupt_task id = SYNCHRONIZED "interrupt" (fn () => TaskQueue.interrupt (! queue) id);
+fun interrupt_task id = SYNCHRONIZED "interrupt"
+  (fn () => TaskQueue.interrupt_external (! queue) id);
 
 end;