# HG changeset patch
# User wenzelm
# Date 1622836876 -7200
# Node ID 4addb970720053cae31851477ccdc673be433ce2
# Parent  1262fefabc9a2b88dc93861405fd1f7524fbf9e9
tuned --- avoid redundant future tasks from already loaded theories;

diff -r 1262fefabc9a -r 4addb9707200 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Fri Jun 04 21:46:14 2021 +0200
+++ b/src/Pure/Thy/thy_info.ML	Fri Jun 04 22:01:16 2021 +0200
@@ -187,10 +187,10 @@
 
 datatype result =
   Result of {theory: theory, exec_id: Document_ID.exec,
-    present: unit -> unit, commit: unit -> unit};
+    present: (unit -> unit) option, commit: unit -> unit};
 
 fun theory_result theory =
-  Result {theory = theory, exec_id = Document_ID.none, present = I, commit = I};
+  Result {theory = theory, exec_id = Document_ID.none, present = NONE, commit = I};
 
 fun result_theory (Result {theory, ...}) = theory;
 fun result_present (Result {present, ...}) = present;
@@ -219,7 +219,7 @@
         let
           val result = body (task_parents deps parents);
           val _ = Par_Exn.release_all (join_theory result);
-          val _ = result_present result ();
+          val _ = (case result_present result of NONE => () | SOME present => present ());
           val _ = result_commit result ();
         in result_theory result end
     | Finished thy => thy)) #> ignore;
@@ -249,10 +249,10 @@
           | Exn.Exn exn => [Exn.Exn exn]));
 
     val results2 = futures
-      |> map_filter (Exn.get_res o Future.join_result)
+      |> map_filter (Option.mapPartial result_present o Exn.get_res o Future.join_result)
       |> Par_List.map'
           {name = "present", sequential = sequential_presentation (Options.default ())}
-          (fn result => Exn.capture (result_present result) ());
+          (fn present => Exn.capture present ());
 
     val results3 = futures
       |> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ());
@@ -358,7 +358,7 @@
     val _ = Output.try_protocol_message (timing_props @ Markup.timing_properties timing_result) []
 
     fun commit () = update_thy deps theory;
-  in Result {theory = theory, exec_id = exec_id, present = present, commit = commit} end;
+  in Result {theory = theory, exec_id = exec_id, present = SOME present, commit = commit} end;
 
 fun check_thy_deps dir name =
   (case lookup_deps name of