tuned;
authorwenzelm
Sun, 06 Nov 2022 18:54:32 +0100
changeset 76472 9a6459e72868
parent 76471 1f0b2d7298d9
child 76473 b45db8030794
tuned;
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;