src/Pure/PIDE/document.ML
changeset 68344 3bb44c25ce8b
parent 68336 09ac56914b29
child 68354 93d3c967802e
     1.1 --- a/src/Pure/PIDE/document.ML	Thu May 31 22:59:08 2018 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Jun 01 10:56:01 2018 +0200
     1.3 @@ -707,17 +707,20 @@
     1.4                      adjust_pos = Position.adjust_offsets adjust,
     1.5                      segments = segments};
     1.6                  in
     1.7 -                  fn () =>
     1.8 +                  fn _ =>
     1.9                      (Thy_Info.apply_presentation presentation_context thy;
    1.10                       commit_consolidated node)
    1.11                  end
    1.12 -              else fn () => commit_consolidated node;
    1.13 +              else fn _ => commit_consolidated node;
    1.14  
    1.15              val result_entry =
    1.16                (case lookup_entry node result_id of
    1.17                  NONE => err_undef "result command entry" result_id
    1.18                | SOME (eval, prints) =>
    1.19 -                  (result_id, SOME (eval, Command.print0 consolidation eval :: prints)));
    1.20 +                  let
    1.21 +                    val print = eval |> Command.print0
    1.22 +                      {pri = Task_Queue.urgent_pri + 1, print_fn = K consolidation};
    1.23 +                  in (result_id, SOME (eval, print :: prints)) end);
    1.24  
    1.25              val assign_update' = assign_update |> assign_update_change result_entry;
    1.26              val node' = node |> assign_entry result_entry;