# HG changeset patch
# User wenzelm
# Date 1502111601 -7200
# Node ID de9c6560c221aea2cede3d35ad488ea897d90e2d
# Parent  d003b44674c1947d4059e03dc96f77b16d9440d4
more synchronized Execution.snapshot;

diff -r d003b44674c1 -r de9c6560c221 src/Pure/PIDE/execution.ML
--- a/src/Pure/PIDE/execution.ML	Mon Aug 07 14:06:24 2017 +0200
+++ b/src/Pure/PIDE/execution.ML	Mon Aug 07 15:13:21 2017 +0200
@@ -12,6 +12,7 @@
   val is_running: Document_ID.execution -> bool
   val is_running_exec: Document_ID.exec -> bool
   val running: Document_ID.execution -> Document_ID.exec -> Future.group list -> bool
+  val snapshot: Document_ID.exec list -> Future.task list
   val peek: Document_ID.exec -> Future.group list
   val cancel: Document_ID.exec -> unit
   type params = {name: string, pos: Position.T, pri: int}
@@ -69,11 +70,17 @@
       val execs' = execs |> ok ? Inttab.update (exec_id, (groups, []));
     in (ok, (execution_id', execs')) end);
 
-fun peek exec_id =
-  (case Inttab.lookup (#2 (get_state ())) exec_id of
+fun exec_groups ((_, execs): state) exec_id =
+  (case Inttab.lookup execs exec_id of
     SOME (groups, _) => groups
   | NONE => []);
 
+fun snapshot exec_ids =
+  change_state_result (fn state =>
+    (maps Future.group_snapshot (maps (exec_groups state) exec_ids), state));
+
+fun peek exec_id = exec_groups (get_state ()) exec_id;
+
 fun cancel exec_id = List.app Future.cancel_group (peek exec_id);
 
 
diff -r d003b44674c1 -r de9c6560c221 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Mon Aug 07 14:06:24 2017 +0200
+++ b/src/Pure/PIDE/protocol.ML	Mon Aug 07 15:13:21 2017 +0200
@@ -100,7 +100,7 @@
           val _ =
             (singleton o Future.forks)
              {name = "Document.update/remove", group = NONE,
-              deps = maps Future.group_snapshot (maps Execution.peek removed),
+              deps = Execution.snapshot removed,
               pri = Task_Queue.urgent_pri + 2, interrupts = false}
              (fn () => (Execution.purge removed; List.app Isabelle_Process.reset_tracing removed));
 
diff -r d003b44674c1 -r de9c6560c221 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Mon Aug 07 14:06:24 2017 +0200
+++ b/src/Pure/Thy/thy_info.ML	Mon Aug 07 15:13:21 2017 +0200
@@ -155,7 +155,7 @@
 fun join_theory (Result {theory, exec_id, ...}) =
   let
     (*toplevel proofs and diags*)
-    val _ = Future.join_tasks (maps Future.group_snapshot (Execution.peek exec_id));
+    val _ = Future.join_tasks (Execution.snapshot [exec_id]);
     (*fully nested proofs*)
     val res = Exn.capture Thm.consolidate_theory theory;
   in res :: map Exn.Exn (maps Task_Queue.group_status (Execution.peek exec_id)) end;