# HG changeset patch
# User wenzelm
# Date 1667485141 -3600
# Node ID 3f16fc68f0f0660dda03c46e6c6ba7f4d7b31e9d
# Parent  cc3911b11b53db6f74c54a57b3f994ca002d48ff
tuned;

diff -r cc3911b11b53 -r 3f16fc68f0f0 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Thu Nov 03 14:50:43 2022 +0100
+++ b/src/Pure/PIDE/document.ML	Thu Nov 03 15:19:01 2022 +0100
@@ -188,17 +188,15 @@
     in SOME (result_id, Toplevel.end_theory Position.none st) handle ERROR _ => NONE end
   else NONE;
 
+fun get_consolidated (Node {consolidated, ...}) = consolidated;
+
 val reset_consolidated =
   map_node (fn (header, keywords, perspective, entries, result, _) =>
     (header, keywords, perspective, entries, result, Lazy.lazy I));
 
-fun commit_consolidated (Node {consolidated, ...}) =
-  (Lazy.force consolidated; Output.status [Markup.markup_only Markup.consolidated]);
-
-fun consolidated_node (Node {consolidated, ...}) = Lazy.is_finished consolidated;
-
 fun could_consolidate node =
-  not (consolidated_node node) andalso is_some (finished_result_theory node);
+  not (Lazy.is_finished (get_consolidated node)) andalso
+  is_some (finished_result_theory node);
 
 fun get_node nodes name = String_Graph.get_node nodes name
   handle String_Graph.UNDEF _ => empty_node;
@@ -745,6 +743,9 @@
       in
         if not active_tasks then
           let
+            fun commit_consolidated () =
+              (Lazy.force (get_consolidated node);
+               Output.status [Markup.markup_only Markup.consolidated]);
             val consolidation =
               if Options.bool options "editor_presentation" then
                 let
@@ -789,10 +790,10 @@
                     let
                       val _ = Output.status [Markup.markup_only Markup.consolidating];
                       val res = Exn.capture (Thy_Info.apply_presentation presentation_context) thy;
-                      val _ = commit_consolidated node;
+                      val _ = commit_consolidated ();
                     in Exn.release res end
                 end
-              else fn _ => commit_consolidated node;
+              else fn _ => commit_consolidated ();
 
             val result_entry =
               (case lookup_entry node result_id of