# HG changeset patch
# User wenzelm
# Date 1667578308 -3600
# Node ID 0901321dd6b2b71c59b86fd5b2bc08c4bee9f467
# Parent  f29056da5903526101fb90e277a6b12150841650
tuned;

diff -r f29056da5903 -r 0901321dd6b2 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Nov 04 16:59:56 2022 +0100
+++ b/src/Pure/PIDE/document.ML	Fri Nov 04 17:11:48 2022 +0100
@@ -720,6 +720,14 @@
 fun removed_execs node0 (command_id, exec_ids) =
   subtract (op =) exec_ids (Command.exec_ids (lookup_entry node0 command_id));
 
+fun node_active node =
+  (node, false) |-> iterate_entries (fn (_, opt_exec) => fn active =>
+    if active then NONE
+    else
+      (case opt_exec of
+        NONE => NONE
+      | SOME (eval, _) => SOME (not (null (Execution.snapshot [Command.eval_exec_id eval])))));
+
 fun presentation_context options the_command_span node_name node : Thy_Info.presentation_context =
   let
     val (_, offsets, rev_segments) =
@@ -762,50 +770,38 @@
 
 fun print_consolidation options the_command_span node_name (assign_update, node) =
   (case finished_result_theory node of
-    SOME (result_id, thy) =>
-      timeit "Document.print_consolidation" (fn () =>
+    NONE => (assign_update, node)
+  | SOME (result_id, thy) => timeit "Document.print_consolidation" (fn () =>
+      if node_active node then (assign_update, node)
+      else
         let
-          val active_tasks =
-            (node, false) |-> iterate_entries (fn (_, opt_exec) => fn active =>
-              if active then NONE
-              else
-                (case opt_exec of
-                  NONE => NONE
-                | SOME (eval, _) =>
-                    SOME (not (null (Execution.snapshot [Command.eval_exec_id eval])))));
-        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 "pide_presentation" then
-                  let val context = presentation_context options the_command_span node_name node in
-                    fn _ =>
-                      let
-                        val _ = Output.status [Markup.markup_only Markup.consolidating];
-                        val res = Exn.capture (Thy_Info.apply_presentation context) thy;
-                        val _ = commit_consolidated ();
-                      in Exn.release res end
-                  end
-                else fn _ => commit_consolidated ();
+          fun commit_consolidated () =
+            (Lazy.force (get_consolidated node);
+             Output.status [Markup.markup_only Markup.consolidated]);
+          val consolidation =
+            if Options.bool options "pide_presentation" then
+              let val context = presentation_context options the_command_span node_name node in
+                fn _ =>
+                  let
+                    val _ = Output.status [Markup.markup_only Markup.consolidating];
+                    val res = Exn.capture (Thy_Info.apply_presentation context) thy;
+                    val _ = commit_consolidated ();
+                  in Exn.release res end
+              end
+            else fn _ => commit_consolidated ();
 
-              val result_entry =
-                (case lookup_entry node result_id of
-                  NONE => err_undef "result command entry" result_id
-                | SOME (eval, prints) =>
-                    let
-                      val print = eval |> Command.print0
-                        {pri = Task_Queue.urgent_pri + 1, print_fn = K consolidation};
-                    in (result_id, SOME (eval, print :: prints)) end);
+          val result_entry =
+            (case lookup_entry node result_id of
+              NONE => err_undef "result command entry" result_id
+            | SOME (eval, prints) =>
+                let
+                  val print = eval |> Command.print0
+                    {pri = Task_Queue.urgent_pri + 1, print_fn = K consolidation};
+                in (result_id, SOME (eval, print :: prints)) end);
 
-              val assign_update' = assign_update |> assign_update_change result_entry;
-              val node' = node |> assign_entry result_entry;
-            in (assign_update', node') end
-          else (assign_update, node)
-        end)
-  | NONE => (assign_update, node));
+          val assign_update' = assign_update |> assign_update_change result_entry;
+          val node' = node |> assign_entry result_entry;
+        in (assign_update', node') end));
 in
 
 fun update old_version_id new_version_id edits consolidate state =