purely functional task_queue.ML -- moved actual interrupt_unsynchronized to 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;
 

--- a/src/Pure/Concurrent/task_queue.ML	Sun Aug 21 13:10:48 2011 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Sun Aug 21 13:23:29 2011 +0200
@@ -31,8 +31,8 @@
   val known_task: queue -> task -> bool
   val all_passive: queue -> bool
   val status: queue -> {ready: int, pending: int, running: int, passive: int}
-  val cancel: queue -> group -> task list
-  val cancel_all: queue -> group list
+  val cancel: queue -> group -> task list * Thread.thread list
+  val cancel_all: queue -> group list * Thread.thread list
   val finish: task -> queue -> bool * queue
   val enqueue_passive: group -> (unit -> bool) -> queue -> task * queue
   val enqueue: string -> group -> task list -> int -> (bool -> bool) -> queue -> task * queue
@@ -249,15 +249,14 @@
 fun cancel (Queue {groups, jobs}) group =
   let
     val _ = cancel_group group Exn.Interrupt;
-    val (tasks, threads) =
+    val running =
       Tasks.fold (fn (task, _) => fn (tasks, threads) =>
           (case get_job jobs task of
             Running thread => (task :: tasks, insert Thread.equal thread threads)
           | Passive _ => (task :: tasks, threads)
           | _ => (tasks, threads)))
         (get_tasks groups (group_id group)) ([], []);
-    val _ = List.app Simple_Thread.interrupt_unsynchronized threads;
-  in tasks end;
+  in running end;
 
 fun cancel_all (Queue {jobs, ...}) =
   let
@@ -270,9 +269,8 @@
           Running t => (insert eq_group group groups, insert Thread.equal t running)
         | _ => (groups, running))
       end;
-    val (running_groups, running) = Task_Graph.fold cancel_job jobs ([], []);
-    val _ = List.app Simple_Thread.interrupt_unsynchronized running;
-  in running_groups end;
+    val running = Task_Graph.fold cancel_job jobs ([], []);
+  in running end;
 
 
 (* finish *)