# HG changeset patch
# User wenzelm
# Date 1313925048 -7200
# Node ID 3b859b573f1a920266dad8a04e973f66f8a56b71
# Parent  eda6aef75939301b754fa3b0e45eb084c591b72d
refined Task_Queue.cancel: passive tasks are considered running due to pending abort operation;

diff -r eda6aef75939 -r 3b859b573f1a src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Sat Aug 20 23:36:18 2011 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Sun Aug 21 13:10:48 2011 +0200
@@ -249,13 +249,15 @@
 fun cancel (Queue {groups, jobs}) group =
   let
     val _ = cancel_group group Exn.Interrupt;
-    val running =
-      Tasks.fold (fn (task, _) =>
-          (case get_job jobs task of Running thread => cons (task, thread) | _ => I))
-        (get_tasks groups (group_id group)) [];
-    val threads = fold (insert Thread.equal o #2) running [];
+    val (tasks, threads) =
+      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 map #1 running end;
+  in tasks end;
 
 fun cancel_all (Queue {jobs, ...}) =
   let