# HG changeset patch
# User wenzelm
# Date 1527843361 -7200
# Node ID 3bb44c25ce8bbe5aac724c1ab5b097eb26ecff95
# Parent  3f60cba346aa6140b28b89f45f4075075c52d97a
clarified priority;

diff -r 3f60cba346aa -r 3bb44c25ce8b src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Thu May 31 22:59:08 2018 +0200
+++ b/src/Pure/PIDE/command.ML	Fri Jun 01 10:56:01 2018 +0200
@@ -22,10 +22,10 @@
   val eval: Keyword.keywords -> Path.T -> (unit -> theory) ->
     blob list * int -> Document_ID.command -> Token.T list -> eval -> eval
   type print
-  val print0: (unit -> unit) -> eval -> print
+  type print_fn = Toplevel.transition -> Toplevel.state -> unit
+  val print0: {pri: int, print_fn: print_fn} -> eval -> print
   val print: bool -> (string * string list) list -> Keyword.keywords -> string ->
     eval -> print list -> print list option
-  type print_fn = Toplevel.transition -> Toplevel.state -> unit
   type print_function =
     {keywords: Keyword.keywords, command_name: string, args: string list, exec_id: Document_ID.exec} ->
       {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option
@@ -342,9 +342,9 @@
 
 in
 
-fun print0 e =
+fun print0 {pri, print_fn} =
   make_print ("", [serial_string ()])
-    {delay = NONE, pri = 0, persistent = true, strict = true, print_fn = fn _ => fn _ => e ()};
+    {delay = NONE, pri = pri, persistent = true, strict = true, print_fn = print_fn};
 
 fun print command_visible command_overlays keywords command_name eval old_prints =
   let
diff -r 3f60cba346aa -r 3bb44c25ce8b src/Pure/PIDE/document.ML
--- 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;