# HG changeset patch
# User wenzelm
# Date 1667757272 -3600
# Node ID 9a6459e72868f6f639e53609c0596fc7a9d924c2
# Parent  1f0b2d7298d9345599733d7c5e3c6975a7cc8ae8
tuned;

diff -r 1f0b2d7298d9 -r 9a6459e72868 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Sun Nov 06 15:28:56 2022 +0100
+++ b/src/Pure/PIDE/document.ML	Sun Nov 06 18:54:32 2022 +0100
@@ -778,8 +778,8 @@
         if finished_eval node then
           let
             val context = presentation_context options the_command_span node_name node;
-            val pr =
-              {pri = Task_Queue.urgent_pri + 1, print_fn = fn _ => fn _ =>
+            val consolidate =
+              Command.print0 {pri = Task_Queue.urgent_pri + 1, print_fn = fn _ => fn _ =>
                 let
                   val _ = Output.status [Markup.markup_only Markup.consolidating];
                   val res = Exn.capture (Thy_Info.apply_presentation context) thy;
@@ -789,7 +789,7 @@
             val result_entry =
               (case lookup_entry node id of
                 NONE => err_undef "result command entry" id
-              | SOME (eval, prints) => (id, SOME (eval, Command.print0 pr eval :: prints)));
+              | SOME (eval, prints) => (id, SOME (eval, consolidate eval :: prints)));
 
             val assign_update' = assign_update |> assign_update_change result_entry;
             val node' = node |> assign_entry result_entry;