src/Pure/Concurrent/future.ML

--- a/src/Pure/Concurrent/future.ML	Sun Aug 21 13:10:48 2011 +0200
+++ b/src/Pure/Concurrent/future.ML	Sun Aug 21 13:23:29 2011 +0200
@@ -186,13 +186,21 @@
 (* cancellation primitives *)
 
 fun cancel_now group = (*requires SYNCHRONIZED*)
-  Task_Queue.cancel (! queue) group;
+  let
+    val (tasks, threads) = Task_Queue.cancel (! queue) group;
+    val _ = List.app Simple_Thread.interrupt_unsynchronized threads;
+  in tasks end;
+
+fun cancel_all () = (*requires SYNCHRONIZED*)
+  let
+    val (groups, threads) = Task_Queue.cancel_all (! queue);
+    val _ = List.app Simple_Thread.interrupt_unsynchronized threads;
+  in groups end;
 
 fun cancel_later group = (*requires SYNCHRONIZED*)
  (Unsynchronized.change canceled (insert Task_Queue.eq_group group);
   broadcast scheduler_event);
 
-
 fun interruptible_task f x =
   (if Multithreading.available then
     Multithreading.with_attributes
@@ -380,7 +388,7 @@
   handle exn =>
     if Exn.is_interrupt exn then
      (Multithreading.tracing 1 (fn () => "Interrupt");
-      List.app cancel_later (Task_Queue.cancel_all (! queue));
+      List.app cancel_later (cancel_all ());
       broadcast_work (); true)
     else reraise exn;