added interrupt_task (external id);
tuned signature;

--- 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;