src/Pure/Concurrent/task_queue.ML

   val running: task -> (unit -> 'a) -> 'a
   val joining: task -> (unit -> 'a) -> 'a
   val waiting: task -> task list -> (unit -> 'a) -> 'a
   type queue
   val empty: queue
+  val group_tasks: queue -> group -> task list
   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 * Thread.thread list
+  val cancel: queue -> group -> 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
   val extend: task -> (bool -> bool) -> queue -> queue option

 datatype queue = Queue of {groups: groups, jobs: jobs};
 
 fun make_queue groups jobs = Queue {groups = groups, jobs = jobs};
 val empty = make_queue Inttab.empty Task_Graph.empty;
 
+fun group_tasks (Queue {groups, ...}) group = Tasks.keys (get_tasks groups (group_id group));
 fun known_task (Queue {jobs, ...}) task = can (Task_Graph.get_entry jobs) task;
 
 
 (* job status *)
 

 
 fun cancel (Queue {groups, jobs}) group =
   let
     val _ = cancel_group group Exn.Interrupt;
     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)) ([], []);
+      Tasks.fold (fn (task, _) =>
+          (case get_job jobs task of Running thread => insert Thread.equal thread | _ => I))
+        (get_tasks groups (group_id group)) [];
   in running end;
 
 fun cancel_all (Queue {jobs, ...}) =
   let
     fun cancel_job (task, (job, _)) (groups, running) =