--- a/src/Pure/Thy/thy_info.ML Mon Jun 07 09:27:01 2021 +0200
+++ b/src/Pure/Thy/thy_info.ML Mon Jun 07 09:36:21 2021 +0200
@@ -197,6 +197,12 @@
fun result_theory (Result {theory, ...}) = theory;
fun result_commit (Result {commit, ...}) = commit;
+datatype task =
+ Task of string list * (theory list -> result) |
+ Finished of theory;
+
+local
+
fun consolidate_theory (Exn.Exn exn) = [Exn.Exn exn]
| consolidate_theory (Exn.Res (Result {theory, exec_id, ...})) =
let
@@ -212,10 +218,7 @@
| SOME (context as {segments, ...}) =>
[Exn.capture (fn () => (apply_presentation context theory; (theory, segments))) ()]);
-
-datatype task =
- Task of string list * (theory list -> result) |
- Finished of theory;
+in
val schedule_theories = Thread_Attributes.uninterruptible (fn _ => fn tasks =>
let
@@ -251,6 +254,8 @@
val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4);
in Par_Exn.release_all present_results end);
+end;
+
(* eval theory *)