# HG changeset patch
# User wenzelm
# Date 1502129123 -7200
# Node ID 6ce1afc0104094952c6a022d101a4a24b7fe44e2
# Parent  de9c6560c221aea2cede3d35ad488ea897d90e2d
more thorough Execution.join, under the assumption that nested Execution.fork only happens from given exed_ids;

diff -r de9c6560c221 -r 6ce1afc01040 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Mon Aug 07 15:13:21 2017 +0200
+++ b/src/Pure/Concurrent/future.ML	Mon Aug 07 20:05:23 2017 +0200
@@ -31,7 +31,6 @@
   val join_result: 'a future -> 'a Exn.result
   val joins: 'a future list -> 'a list
   val join: 'a future -> 'a
-  val join_tasks: task list -> unit
   val task_context: string -> group -> ('a -> 'b) -> 'a -> 'b
   val value_result: 'a Exn.result -> 'a future
   val value: 'a -> 'a future
@@ -532,14 +531,6 @@
 fun joins xs = Par_Exn.release_all (join_results xs);
 fun join x = Exn.release (join_result x);
 
-fun join_tasks tasks =
-  if null tasks then ()
-  else
-    (singleton o forks)
-      {name = "join_tasks", group = SOME (new_group NONE),
-        deps = tasks, pri = 0, interrupts = false} I
-    |> join;
-
 
 (* task context for running thread *)
 
diff -r de9c6560c221 -r 6ce1afc01040 src/Pure/PIDE/execution.ML
--- a/src/Pure/PIDE/execution.ML	Mon Aug 07 15:13:21 2017 +0200
+++ b/src/Pure/PIDE/execution.ML	Mon Aug 07 20:05:23 2017 +0200
@@ -13,6 +13,7 @@
   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 join: Document_ID.exec list -> unit
   val peek: Document_ID.exec -> Future.group list
   val cancel: Document_ID.exec -> unit
   type params = {name: string, pos: Position.T, pri: int}
@@ -58,7 +59,7 @@
 fun is_running execution_id = execution_id = #1 (get_state ());
 
 
-(* execs *)
+(* running execs *)
 
 fun is_running_exec exec_id =
   Inttab.defined (#2 (get_state ())) exec_id;
@@ -70,6 +71,9 @@
       val execs' = execs |> ok ? Inttab.update (exec_id, (groups, []));
     in (ok, (execution_id', execs')) end);
 
+
+(* exec groups and tasks *)
+
 fun exec_groups ((_, execs): state) exec_id =
   (case Inttab.lookup execs exec_id of
     SOME (groups, _) => groups
@@ -79,6 +83,15 @@
   change_state_result (fn state =>
     (maps Future.group_snapshot (maps (exec_groups state) exec_ids), state));
 
+fun join exec_ids =
+  (case snapshot exec_ids of
+    [] => ()
+  | tasks =>
+      ((singleton o Future.forks)
+        {name = "Execution.join", group = SOME (Future.new_group NONE),
+          deps = tasks, pri = 0, interrupts = false} I
+      |> Future.join; join exec_ids));
+
 fun peek exec_id = exec_groups (get_state ()) exec_id;
 
 fun cancel exec_id = List.app Future.cancel_group (peek exec_id);
diff -r de9c6560c221 -r 6ce1afc01040 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Mon Aug 07 15:13:21 2017 +0200
+++ b/src/Pure/Thy/thy_info.ML	Mon Aug 07 20:05:23 2017 +0200
@@ -154,11 +154,10 @@
 
 fun join_theory (Result {theory, exec_id, ...}) =
   let
-    (*toplevel proofs and diags*)
-    val _ = Future.join_tasks (Execution.snapshot [exec_id]);
-    (*fully nested proofs*)
+    val _ = Execution.join [exec_id];
     val res = Exn.capture Thm.consolidate_theory theory;
-  in res :: map Exn.Exn (maps Task_Queue.group_status (Execution.peek exec_id)) end;
+    val errs = maps Task_Queue.group_status (Execution.peek exec_id);
+  in res :: map Exn.Exn errs end;
 
 datatype task =
   Task of Path.T * string list * (theory list -> result) |