# HG changeset patch
# User wenzelm
# Date 1502187689 -7200
# Node ID 53a6c5d4d03e0fe36a3035d8096cfa736f31ed42
# Parent  753eb5b833705444ac0639646156dc66de6fd231
clarified signature;

diff -r 753eb5b83370 -r 53a6c5d4d03e src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Tue Aug 08 11:49:35 2017 +0200
+++ b/src/Pure/Concurrent/future.ML	Tue Aug 08 12:21:29 2017 +0200
@@ -40,7 +40,7 @@
   val promise: (unit -> unit) -> 'a future
   val fulfill_result: 'a future -> 'a Exn.result -> unit
   val fulfill: 'a future -> 'a -> unit
-  val group_snapshot: group -> task list
+  val snapshot: group list -> task list
   val shutdown: unit -> unit
 end;
 
@@ -638,11 +638,11 @@
 fun fulfill x res = fulfill_result x (Exn.Res res);
 
 
-(* group snapshot *)
+(* snapshot: current tasks of groups *)
 
-fun group_snapshot group =
-  SYNCHRONIZED "group_snapshot" (fn () =>
-    Task_Queue.group_tasks (! queue) group);
+fun snapshot groups =
+  SYNCHRONIZED "snapshot" (fn () =>
+    Task_Queue.group_tasks (! queue) groups);
 
 
 (* shutdown *)
diff -r 753eb5b83370 -r 53a6c5d4d03e src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Tue Aug 08 11:49:35 2017 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Tue Aug 08 12:21:29 2017 +0200
@@ -29,7 +29,7 @@
   val waiting: task -> task list -> (unit -> 'a) -> 'a
   type queue
   val empty: queue
-  val group_tasks: queue -> group -> task list
+  val group_tasks: queue -> group list -> task list
   val known_task: queue -> task -> bool
   val all_passive: queue -> bool
   val status: queue -> {ready: int, pending: int, running: int, passive: int, urgent: int}
@@ -222,7 +222,11 @@
 fun make_queue groups jobs urgent = Queue {groups = groups, jobs = jobs, urgent = urgent};
 val empty = make_queue Inttab.empty Task_Graph.empty 0;
 
-fun group_tasks (Queue {groups, ...}) group = Tasks.keys (get_tasks groups (group_id group));
+fun group_tasks (Queue {groups, ...}) gs =
+  fold (fn g => fn tasks => Tasks.merge (op =) (tasks, get_tasks groups (group_id g)))
+    gs Tasks.empty
+  |> Tasks.keys;
+
 fun known_task (Queue {jobs, ...}) task = can (Task_Graph.get_entry jobs) task;
 
 
diff -r 753eb5b83370 -r 53a6c5d4d03e src/Pure/PIDE/execution.ML
--- a/src/Pure/PIDE/execution.ML	Tue Aug 08 11:49:35 2017 +0200
+++ b/src/Pure/PIDE/execution.ML	Tue Aug 08 12:21:29 2017 +0200
@@ -80,8 +80,7 @@
   | NONE => []);
 
 fun snapshot exec_ids =
-  change_state_result (fn state =>
-    (maps Future.group_snapshot (maps (exec_groups state) exec_ids), state));
+  change_state_result (`(fn state => Future.snapshot (maps (exec_groups state) exec_ids)));
 
 fun join exec_ids =
   (case snapshot exec_ids of