clarified priority;
authorwenzelm
Fri Jun 01 10:56:01 2018 +0200 (14 months ago)
changeset 683443bb44c25ce8b
parent 68338 3f60cba346aa
child 68345 5bc1e1ac7955
clarified priority;
src/Pure/PIDE/command.ML
src/Pure/PIDE/document.ML
     1.1 --- a/src/Pure/PIDE/command.ML	Thu May 31 22:59:08 2018 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Fri Jun 01 10:56:01 2018 +0200
     1.3 @@ -22,10 +22,10 @@
     1.4    val eval: Keyword.keywords -> Path.T -> (unit -> theory) ->
     1.5      blob list * int -> Document_ID.command -> Token.T list -> eval -> eval
     1.6    type print
     1.7 -  val print0: (unit -> unit) -> eval -> print
     1.8 +  type print_fn = Toplevel.transition -> Toplevel.state -> unit
     1.9 +  val print0: {pri: int, print_fn: print_fn} -> eval -> print
    1.10    val print: bool -> (string * string list) list -> Keyword.keywords -> string ->
    1.11      eval -> print list -> print list option
    1.12 -  type print_fn = Toplevel.transition -> Toplevel.state -> unit
    1.13    type print_function =
    1.14      {keywords: Keyword.keywords, command_name: string, args: string list, exec_id: Document_ID.exec} ->
    1.15        {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option
    1.16 @@ -342,9 +342,9 @@
    1.17  
    1.18  in
    1.19  
    1.20 -fun print0 e =
    1.21 +fun print0 {pri, print_fn} =
    1.22    make_print ("", [serial_string ()])
    1.23 -    {delay = NONE, pri = 0, persistent = true, strict = true, print_fn = fn _ => fn _ => e ()};
    1.24 +    {delay = NONE, pri = pri, persistent = true, strict = true, print_fn = print_fn};
    1.25  
    1.26  fun print command_visible command_overlays keywords command_name eval old_prints =
    1.27    let
     2.1 --- a/src/Pure/PIDE/document.ML	Thu May 31 22:59:08 2018 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Fri Jun 01 10:56:01 2018 +0200
     2.3 @@ -707,17 +707,20 @@
     2.4                      adjust_pos = Position.adjust_offsets adjust,
     2.5                      segments = segments};
     2.6                  in
     2.7 -                  fn () =>
     2.8 +                  fn _ =>
     2.9                      (Thy_Info.apply_presentation presentation_context thy;
    2.10                       commit_consolidated node)
    2.11                  end
    2.12 -              else fn () => commit_consolidated node;
    2.13 +              else fn _ => commit_consolidated node;
    2.14  
    2.15              val result_entry =
    2.16                (case lookup_entry node result_id of
    2.17                  NONE => err_undef "result command entry" result_id
    2.18                | SOME (eval, prints) =>
    2.19 -                  (result_id, SOME (eval, Command.print0 consolidation eval :: prints)));
    2.20 +                  let
    2.21 +                    val print = eval |> Command.print0
    2.22 +                      {pri = Task_Queue.urgent_pri + 1, print_fn = K consolidation};
    2.23 +                  in (result_id, SOME (eval, print :: prints)) end);
    2.24  
    2.25              val assign_update' = assign_update |> assign_update_change result_entry;
    2.26              val node' = node |> assign_entry result_entry;