src/Pure/PIDE/document.ML
changeset 68344 3bb44c25ce8b
parent 68336 09ac56914b29
child 68354 93d3c967802e
--- a/src/Pure/PIDE/document.ML	Thu May 31 22:59:08 2018 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Jun 01 10:56:01 2018 +0200
@@ -707,17 +707,20 @@
                     adjust_pos = Position.adjust_offsets adjust,
                     segments = segments};
                 in
-                  fn () =>
+                  fn _ =>
                     (Thy_Info.apply_presentation presentation_context thy;
                      commit_consolidated node)
                 end
-              else fn () => commit_consolidated node;
+              else fn _ => commit_consolidated node;
 
             val result_entry =
               (case lookup_entry node result_id of
                 NONE => err_undef "result command entry" result_id
               | SOME (eval, prints) =>
-                  (result_id, SOME (eval, Command.print0 consolidation 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;