refined Task_Queue.cancel: passive tasks are considered running due to pending abort operation;
--- 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