# HG changeset patch
# User wenzelm
# Date 1622981520 -7200
# Node ID df0fd744e6bb3cdd2b99634cbd60a01a04698583
# Parent  43882e34c038db7b5b8a12575b34a4846fc622be
tuned;

diff -r 43882e34c038 -r df0fd744e6bb src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sat Jun 05 21:01:00 2021 +0200
+++ b/src/Pure/Thy/thy_info.ML	Sun Jun 06 14:12:00 2021 +0200
@@ -196,20 +196,18 @@
 fun result_present (Result {present, ...}) = present;
 fun result_commit (Result {commit, ...}) = commit;
 
-fun join_theory (Result {theory, exec_id, ...}) =
-  let
-    val _ = Execution.join [exec_id];
-    val res = Exn.capture Thm.consolidate_theory theory;
-    val exns = maps Task_Queue.group_status (Execution.peek exec_id);
-  in res :: map Exn.Exn exns end;
+fun consolidate_theory (Exn.Exn exn) = [Exn.Exn exn]
+  | consolidate_theory (Exn.Res (Result {theory, exec_id, ...})) =
+      let
+        val _ = Execution.join [exec_id];
+        val res = Exn.capture Thm.consolidate_theory theory;
+        val exns = maps Task_Queue.group_status (Execution.peek exec_id);
+      in res :: map Exn.Exn exns end;
 
 datatype task =
   Task of string list * (theory list -> result) |
   Finished of theory;
 
-fun task_finished (Task _) = false
-  | task_finished (Finished _) = true;
-
 fun task_parents deps (parents: string list) = map (the o AList.lookup (op =) deps) parents;
 
 val schedule_seq =
@@ -218,7 +216,7 @@
       Task (parents, body) =>
         let
           val result = body (task_parents deps parents);
-          val _ = Par_Exn.release_all (join_theory result);
+          val _ = Par_Exn.release_all (consolidate_theory (Exn.Res result));
           val _ = (case result_present result of NONE => () | SOME present => present ());
           val _ = result_commit result ();
         in result_theory result end
@@ -242,11 +240,7 @@
                         " (unresolved " ^ commas_quote (map #1 bad) ^ ")")))
         | Finished theory => Future.value (theory_result theory)));
 
-    val results1 = futures
-      |> maps (fn future =>
-          (case Future.join_result future of
-            Exn.Res result => join_theory result
-          | Exn.Exn exn => [Exn.Exn exn]));
+    val results1 = futures |> maps (consolidate_theory o Future.join_result);
 
     val results2 = futures
       |> map_filter (Option.mapPartial result_present o Exn.get_res o Future.join_result)
@@ -257,11 +251,9 @@
     val results3 = futures
       |> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ());
 
-    (* FIXME avoid global Execution.reset (!??) *)
     val results4 = map Exn.Exn (maps Task_Queue.group_status (Execution.reset ()));
 
-    val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4);
-  in () end);
+  in ignore (Par_Exn.release_all (results1 @ results2 @ results3 @ results4)) end);
 
 
 (* eval theory *)
@@ -378,6 +370,9 @@
             | SOME theory => Resources.loaded_files_current theory);
       in (current, deps', theory_pos', imports', keywords') end);
 
+fun task_finished (Task _) = false
+  | task_finished (Finished _) = true;
+
 in
 
 fun require_thys options initiators qualifier dir strs tasks =