refined Task_Queue.cancel: passive tasks are considered running due to pending abort operation;
authorwenzelm
Sun, 21 Aug 2011 13:10:48 +0200
changeset 44340 3b859b573f1a
parent 44339 eda6aef75939
child 44341 a93d25fb14fc
refined Task_Queue.cancel: passive tasks are considered running due to pending abort operation;
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