refined Task_Queue.cancel: passive tasks are considered running due to pending abort operation;
authorwenzelm
Sun Aug 21 13:10:48 2011 +0200 (2011-08-21)
changeset 443403b859b573f1a
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
     1.1 --- a/src/Pure/Concurrent/task_queue.ML	Sat Aug 20 23:36:18 2011 +0200
     1.2 +++ b/src/Pure/Concurrent/task_queue.ML	Sun Aug 21 13:10:48 2011 +0200
     1.3 @@ -249,13 +249,15 @@
     1.4  fun cancel (Queue {groups, jobs}) group =
     1.5    let
     1.6      val _ = cancel_group group Exn.Interrupt;
     1.7 -    val running =
     1.8 -      Tasks.fold (fn (task, _) =>
     1.9 -          (case get_job jobs task of Running thread => cons (task, thread) | _ => I))
    1.10 -        (get_tasks groups (group_id group)) [];
    1.11 -    val threads = fold (insert Thread.equal o #2) running [];
    1.12 +    val (tasks, threads) =
    1.13 +      Tasks.fold (fn (task, _) => fn (tasks, threads) =>
    1.14 +          (case get_job jobs task of
    1.15 +            Running thread => (task :: tasks, insert Thread.equal thread threads)
    1.16 +          | Passive _ => (task :: tasks, threads)
    1.17 +          | _ => (tasks, threads)))
    1.18 +        (get_tasks groups (group_id group)) ([], []);
    1.19      val _ = List.app Simple_Thread.interrupt_unsynchronized threads;
    1.20 -  in map #1 running end;
    1.21 +  in tasks end;
    1.22  
    1.23  fun cancel_all (Queue {jobs, ...}) =
    1.24    let