# HG changeset patch
# User wenzelm
# Date 1527800348 -7200
# Node ID 3f60cba346aa6140b28b89f45f4075075c52d97a
# Parent  9946707cf32978ed0d300baafde22a02a9df1bed# Parent  70818e1bb1511563aa662fc425973faabcb1fe7d
merged

diff -r 9946707cf329 -r 3f60cba346aa src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Thu May 31 10:59:54 2018 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Thu May 31 22:59:08 2018 +0200
@@ -92,13 +92,13 @@
   end;
 
 val _ =
-  Outer_Syntax.command @{command_keyword spark_open_vcg}
+  Outer_Syntax.command \<^command_keyword>\<open>spark_open_vcg\<close>
     "open a new SPARK environment and load a SPARK-generated .vcg file"
     (Resources.provide_parse_files "spark_open_vcg" -- Parse.parname
       >> (Toplevel.theory o spark_open Fdl_Lexer.vcg_header));
 
 val _ =
-  Outer_Syntax.command @{command_keyword spark_open}
+  Outer_Syntax.command \<^command_keyword>\<open>spark_open\<close>
     "open a new SPARK environment and load a SPARK-generated .siv file"
     (Resources.provide_parse_files "spark_open" -- Parse.parname
       >> (Toplevel.theory o spark_open Fdl_Lexer.siv_header));
@@ -107,13 +107,13 @@
   (Args.parens (Parse.list1 Parse.name) --| Args.colon -- Parse.name);
 
 val _ =
-  Outer_Syntax.command @{command_keyword spark_proof_functions}
+  Outer_Syntax.command \<^command_keyword>\<open>spark_proof_functions\<close>
     "associate SPARK proof functions with terms"
     (Scan.repeat1 (Parse.name -- (pfun_type --| Args.$$$ "=" -- Parse.term)) >>
       (Toplevel.theory o fold add_proof_fun_cmd));
 
 val _ =
-  Outer_Syntax.command @{command_keyword spark_types}
+  Outer_Syntax.command \<^command_keyword>\<open>spark_types\<close>
     "associate SPARK types with types"
     (Scan.repeat1 (Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.typ --
        Scan.optional (Args.parens (Parse.list1
@@ -121,12 +121,12 @@
        (Toplevel.theory o fold add_spark_type_cmd));
 
 val _ =
-  Outer_Syntax.local_theory_to_proof @{command_keyword spark_vc}
+  Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>spark_vc\<close>
     "enter into proof mode for a specific verification condition"
     (Parse.name >> prove_vc);
 
 val _ =
-  Outer_Syntax.command @{command_keyword spark_status}
+  Outer_Syntax.command \<^command_keyword>\<open>spark_status\<close>
     "show the name and state of all loaded verification conditions"
     (Scan.optional
        (Args.parens
@@ -136,10 +136,10 @@
         Toplevel.keep (fn state => show_status (Toplevel.theory_of state) args)))
 
 val _ =
-  Outer_Syntax.command @{command_keyword spark_end}
+  Outer_Syntax.command \<^command_keyword>\<open>spark_end\<close>
     "close the current SPARK environment"
-    (Scan.optional (@{keyword "("} |-- Parse.!!!
-         (Parse.reserved "incomplete" --| @{keyword ")"}) >> K true) false >>
+    (Scan.optional (\<^keyword>\<open>(\<close> |-- Parse.!!!
+         (Parse.reserved "incomplete" --| \<^keyword>\<open>)\<close>) >> K true) false >>
        (Toplevel.theory o SPARK_VCs.close));
 
 val _ = Theory.setup (Theory.at_end (fn thy =>
diff -r 9946707cf329 -r 3f60cba346aa src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Thu May 31 10:59:54 2018 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Thu May 31 22:59:08 2018 +0200
@@ -101,7 +101,7 @@
     val T = HOLogic.dest_setT setT;
     val U = HOLogic.dest_setT (fastype_of u)
   in
-    Const (@{const_name Sigma}, setT --> (T --> HOLogic.mk_setT U) -->
+    Const (\<^const_name>\<open>Sigma\<close>, setT --> (T --> HOLogic.mk_setT U) -->
       HOLogic.mk_setT (HOLogic.mk_prodT (T, U))) $ t $ Abs ("", T, u)
   end;
 
@@ -150,7 +150,7 @@
   in (zs, (fold (Symtab.update o apsnd (rpair ty)) (xs ~~ zs) tab, ctxt')) end;
 
 fun get_record_info thy T = (case Record.dest_recTs T of
-    [(tyname, [@{typ unit}])] =>
+    [(tyname, [\<^typ>\<open>unit\<close>])] =>
       Record.get_info thy (Long_Name.qualifier tyname)
   | _ => NONE);
 
@@ -177,9 +177,9 @@
     val cs = map Const (the (BNF_LFP_Compat.get_constrs thy tyname'));
     val k = length cs;
     val T = Type (tyname', []);
-    val p = Const (@{const_name pos}, T --> HOLogic.intT);
-    val v = Const (@{const_name val}, HOLogic.intT --> T);
-    val card = Const (@{const_name card},
+    val p = Const (\<^const_name>\<open>pos\<close>, T --> HOLogic.intT);
+    val v = Const (\<^const_name>\<open>val\<close>, HOLogic.intT --> T);
+    val card = Const (\<^const_name>\<open>card\<close>,
       HOLogic.mk_setT T --> HOLogic.natT) $ HOLogic.mk_UNIV T;
 
     fun mk_binrel_def s f = Logic.mk_equals
@@ -190,7 +190,7 @@
 
     val (((def1, def2), def3), lthy) = thy |>
 
-      Class.instantiation ([tyname'], [], @{sort spark_enum}) |>
+      Class.instantiation ([tyname'], [], \<^sort>\<open>spark_enum\<close>) |>
 
       define_overloaded ("pos_" ^ tyname ^ "_def", Logic.mk_equals
         (p,
@@ -199,9 +199,9 @@
            map (HOLogic.mk_number HOLogic.intT) (0 upto k - 1)))) ||>>
 
       define_overloaded ("less_eq_" ^ tyname ^ "_def",
-        mk_binrel_def @{const_name less_eq} p) ||>>
+        mk_binrel_def \<^const_name>\<open>less_eq\<close> p) ||>>
       define_overloaded ("less_" ^ tyname ^ "_def",
-        mk_binrel_def @{const_name less} p);
+        mk_binrel_def \<^const_name>\<open>less\<close> p);
 
     val UNIV_eq = Goal.prove lthy [] []
       (HOLogic.mk_Trueprop (HOLogic.mk_eq
@@ -214,7 +214,7 @@
          ALLGOALS (asm_full_simp_tac ctxt));
 
     val finite_UNIV = Goal.prove lthy [] []
-      (HOLogic.mk_Trueprop (Const (@{const_name finite},
+      (HOLogic.mk_Trueprop (Const (\<^const_name>\<open>finite\<close>,
          HOLogic.mk_setT T --> HOLogic.boolT) $ HOLogic.mk_UNIV T))
       (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [UNIV_eq]) 1);
 
@@ -225,13 +225,13 @@
 
     val range_pos = Goal.prove lthy [] []
       (HOLogic.mk_Trueprop (HOLogic.mk_eq
-         (Const (@{const_name image}, (T --> HOLogic.intT) -->
+         (Const (\<^const_name>\<open>image\<close>, (T --> HOLogic.intT) -->
             HOLogic.mk_setT T --> HOLogic.mk_setT HOLogic.intT) $
               p $ HOLogic.mk_UNIV T,
-          Const (@{const_name atLeastLessThan}, HOLogic.intT -->
+          Const (\<^const_name>\<open>atLeastLessThan\<close>, HOLogic.intT -->
             HOLogic.intT --> HOLogic.mk_setT HOLogic.intT) $
               HOLogic.mk_number HOLogic.intT 0 $
-              (@{term int} $ card))))
+              (\<^term>\<open>int\<close> $ card))))
       (fn {context = ctxt, ...} =>
          simp_tac (ctxt addsimps [card_UNIV]) 1 THEN
          simp_tac (ctxt addsimps [UNIV_eq, def1]) 1 THEN
@@ -264,12 +264,12 @@
 
     val first_el = Goal.prove lthy' [] []
       (HOLogic.mk_Trueprop (HOLogic.mk_eq
-         (Const (@{const_name first_el}, T), hd cs)))
+         (Const (\<^const_name>\<open>first_el\<close>, T), hd cs)))
       (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [@{thm first_el_def}, hd val_eqs]) 1);
 
     val last_el = Goal.prove lthy' [] []
       (HOLogic.mk_Trueprop (HOLogic.mk_eq
-         (Const (@{const_name last_el}, T), List.last cs)))
+         (Const (\<^const_name>\<open>last_el\<close>, T), List.last cs)))
       (fn {context = ctxt, ...} =>
         simp_tac (ctxt addsimps [@{thm last_el_def}, List.last val_eqs, card_UNIV]) 1);
   in
@@ -414,43 +414,43 @@
       | tm_of vs (Funct ("<>", [e, e'])) = (HOLogic.mk_not
           (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e'))), booleanN)
 
-      | tm_of vs (Funct ("<", [e, e'])) = (HOLogic.mk_binrel @{const_name less}
+      | tm_of vs (Funct ("<", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less\<close>
           (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
 
-      | tm_of vs (Funct (">", [e, e'])) = (HOLogic.mk_binrel @{const_name less}
+      | tm_of vs (Funct (">", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less\<close>
           (fst (tm_of vs e'), fst (tm_of vs e)), booleanN)
 
-      | tm_of vs (Funct ("<=", [e, e'])) = (HOLogic.mk_binrel @{const_name less_eq}
+      | tm_of vs (Funct ("<=", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less_eq\<close>
           (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
 
-      | tm_of vs (Funct (">=", [e, e'])) = (HOLogic.mk_binrel @{const_name less_eq}
+      | tm_of vs (Funct (">=", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less_eq\<close>
           (fst (tm_of vs e'), fst (tm_of vs e)), booleanN)
 
-      | tm_of vs (Funct ("+", [e, e'])) = (HOLogic.mk_binop @{const_name plus}
+      | tm_of vs (Funct ("+", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>plus\<close>
           (fst (tm_of vs e), fst (tm_of vs e')), integerN)
 
-      | tm_of vs (Funct ("-", [e, e'])) = (HOLogic.mk_binop @{const_name minus}
+      | tm_of vs (Funct ("-", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>minus\<close>
           (fst (tm_of vs e), fst (tm_of vs e')), integerN)
 
-      | tm_of vs (Funct ("*", [e, e'])) = (HOLogic.mk_binop @{const_name times}
+      | tm_of vs (Funct ("*", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>times\<close>
           (fst (tm_of vs e), fst (tm_of vs e')), integerN)
 
-      | tm_of vs (Funct ("/", [e, e'])) = (HOLogic.mk_binop @{const_name divide}
+      | tm_of vs (Funct ("/", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>divide\<close>
           (fst (tm_of vs e), fst (tm_of vs e')), integerN)
 
-      | tm_of vs (Funct ("div", [e, e'])) = (HOLogic.mk_binop @{const_name sdiv}
+      | tm_of vs (Funct ("div", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>sdiv\<close>
           (fst (tm_of vs e), fst (tm_of vs e')), integerN)
 
-      | tm_of vs (Funct ("mod", [e, e'])) = (HOLogic.mk_binop @{const_name modulo}
+      | tm_of vs (Funct ("mod", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>modulo\<close>
           (fst (tm_of vs e), fst (tm_of vs e')), integerN)
 
       | tm_of vs (Funct ("-", [e])) =
-          (mk_unop @{const_name uminus} (fst (tm_of vs e)), integerN)
+          (mk_unop \<^const_name>\<open>uminus\<close> (fst (tm_of vs e)), integerN)
 
       | tm_of vs (Funct ("**", [e, e'])) =
-          (Const (@{const_name power}, HOLogic.intT --> HOLogic.natT -->
+          (Const (\<^const_name>\<open>power\<close>, HOLogic.intT --> HOLogic.natT -->
              HOLogic.intT) $ fst (tm_of vs e) $
-               (@{const nat} $ fst (tm_of vs e')), integerN)
+               (\<^const>\<open>nat\<close> $ fst (tm_of vs e')), integerN)
 
       | tm_of (tab, _) (Ident s) =
           (case Symtab.lookup tab s of
@@ -528,7 +528,7 @@
           (* enumeration type to integer *)
           (case try (unsuffix "__pos") s of
              SOME tyname => (case es of
-               [e] => (Const (@{const_name pos},
+               [e] => (Const (\<^const_name>\<open>pos\<close>,
                    mk_type thy prfx tyname --> HOLogic.intT) $ fst (tm_of vs e),
                  integerN)
              | _ => error ("Function " ^ s ^ " expects one argument"))
@@ -537,7 +537,7 @@
           (* integer to enumeration type *)
           (case try (unsuffix "__val") s of
              SOME tyname => (case es of
-               [e] => (Const (@{const_name val},
+               [e] => (Const (\<^const_name>\<open>val\<close>,
                    HOLogic.intT --> mk_type thy prfx tyname) $ fst (tm_of vs e),
                  tyname)
              | _ => error ("Function " ^ s ^ " expects one argument"))
@@ -550,8 +550,8 @@
                   val (t, tyname) = tm_of vs e;
                   val T = mk_type thy prfx tyname
                 in (Const
-                  (if s = "succ" then @{const_name succ}
-                   else @{const_name pred}, T --> T) $ t, tyname)
+                  (if s = "succ" then \<^const_name>\<open>succ\<close>
+                   else \<^const_name>\<open>pred\<close>, T --> T) $ t, tyname)
                 end
             | _ => error ("Function " ^ s ^ " expects one argument"))
 
@@ -580,7 +580,7 @@
                   val U = mk_type thy prfx elty;
                   val fT = T --> U
                 in
-                  (Const (@{const_name fun_upd}, fT --> T --> U --> fT) $
+                  (Const (\<^const_name>\<open>fun_upd\<close>, fT --> T --> U --> fT) $
                      t $ foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es) $
                        fst (tm_of vs e'),
                    ty)
@@ -628,7 +628,7 @@
                  val T = foldr1 HOLogic.mk_prodT Ts;
                  val U = mk_type thy prfx elty;
                  fun mk_idx' T (e, NONE) = HOLogic.mk_set T [fst (tm_of vs e)]
-                   | mk_idx' T (e, SOME e') = Const (@{const_name atLeastAtMost},
+                   | mk_idx' T (e, SOME e') = Const (\<^const_name>\<open>atLeastAtMost\<close>,
                        T --> T --> HOLogic.mk_setT T) $
                          fst (tm_of vs e) $ fst (tm_of vs e');
                  fun mk_idx idx =
@@ -638,22 +638,22 @@
                  fun mk_upd (idxs, e) t =
                    if length idxs = 1 andalso forall (is_none o snd) (hd idxs)
                    then
-                     Const (@{const_name fun_upd}, (T --> U) -->
+                     Const (\<^const_name>\<open>fun_upd\<close>, (T --> U) -->
                          T --> U --> T --> U) $ t $
                        foldl1 HOLogic.mk_prod
                          (map (fst o tm_of vs o fst) (hd idxs)) $
                        fst (tm_of vs e)
                    else
-                     Const (@{const_name fun_upds}, (T --> U) -->
+                     Const (\<^const_name>\<open>fun_upds\<close>, (T --> U) -->
                          HOLogic.mk_setT T --> U --> T --> U) $ t $
-                       foldl1 (HOLogic.mk_binop @{const_name sup})
+                       foldl1 (HOLogic.mk_binop \<^const_name>\<open>sup\<close>)
                          (map mk_idx idxs) $
                        fst (tm_of vs e)
                in
                  (fold mk_upd assocs
                     (case default of
                        SOME e => Abs ("x", T, fst (tm_of vs e))
-                     | NONE => Const (@{const_name undefined}, T --> U)),
+                     | NONE => Const (\<^const_name>\<open>undefined\<close>, T --> U)),
                   s)
                end
            | _ => error (s ^ " is not an array type"))
@@ -973,7 +973,7 @@
              \because their proofs contain oracles:" proved'));
           val prv_path = Path.ext "prv" path;
           val _ =
-            if File.exists prv_path orelse Options.default_bool @{system_option spark_prv} then
+            if File.exists prv_path orelse Options.default_bool \<^system_option>\<open>spark_prv\<close> then
               File.write prv_path
                (implode (map (fn (s, _) => snd (strip_number s) ^
                   " -- proved by " ^ Distribution.version ^ "\n") proved''))
@@ -1096,8 +1096,8 @@
 
     val (((defs', vars''), ivars), (ids, thy')) =
       ((Symtab.empty |>
-        Symtab.update ("false", (@{term False}, booleanN)) |>
-        Symtab.update ("true", (@{term True}, booleanN)),
+        Symtab.update ("false", (\<^term>\<open>False\<close>, booleanN)) |>
+        Symtab.update ("true", (\<^term>\<open>True\<close>, booleanN)),
         Name.context),
        thy |> Sign.add_path
          ((if prfx' = "" then "" else prfx' ^ "__") ^ Long_Name.base_name ident)) |>
diff -r 9946707cf329 -r 3f60cba346aa src/Pure/ML/ml_console.scala
--- a/src/Pure/ML/ml_console.scala	Thu May 31 10:59:54 2018 +0200
+++ b/src/Pure/ML/ml_console.scala	Thu May 31 22:59:08 2018 +0200
@@ -54,8 +54,10 @@
       if (!no_build && !raw_ml_system) {
         val progress = new Console_Progress()
         val rc =
-          Build.build_logic(options, logic, build_heap = true, progress = progress,
-            dirs = dirs, system_mode = system_mode)
+          progress.interrupt_handler {
+            Build.build_logic(options, logic, build_heap = true, progress = progress,
+              dirs = dirs, system_mode = system_mode)
+          }
         if (rc != 0) sys.exit(rc)
       }
 
diff -r 9946707cf329 -r 3f60cba346aa src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Thu May 31 10:59:54 2018 +0200
+++ b/src/Pure/PIDE/command.ML	Thu May 31 22:59:08 2018 +0200
@@ -22,6 +22,7 @@
   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
   val print: bool -> (string * string list) list -> Keyword.keywords -> string ->
     eval -> print list -> print list option
   type print_fn = Toplevel.transition -> Toplevel.state -> unit
@@ -317,35 +318,39 @@
 
 val overlay_ord = prod_ord string_ord (list_ord string_ord);
 
+fun make_print (name, args) {delay, pri, persistent, strict, print_fn} eval =
+  let
+    val exec_id = Document_ID.make ();
+    fun process () =
+      let
+        val {failed, command, state = st', ...} = eval_result eval;
+        val tr = Toplevel.exec_id exec_id command;
+        val opt_context = try Toplevel.generic_theory_of st';
+      in
+        if failed andalso strict then ()
+        else print_error tr opt_context (fn () => print_fn tr st')
+      end;
+  in
+    Print {
+      name = name, args = args, delay = delay, pri = pri, persistent = persistent,
+      exec_id = exec_id, print_process = Lazy.lazy_name "Command.print" process}
+  end;
+
+fun bad_print name_args exn =
+  make_print name_args {delay = NONE, pri = 0, persistent = false,
+    strict = false, print_fn = fn _ => fn _ => Exn.reraise exn};
+
 in
 
+fun print0 e =
+  make_print ("", [serial_string ()])
+    {delay = NONE, pri = 0, persistent = true, strict = true, print_fn = fn _ => fn _ => e ()};
+
 fun print command_visible command_overlays keywords command_name eval old_prints =
   let
     val print_functions = Synchronized.value print_functions;
 
-    fun make_print name args {delay, pri, persistent, strict, print_fn} =
-      let
-        val exec_id = Document_ID.make ();
-        fun process () =
-          let
-            val {failed, command, state = st', ...} = eval_result eval;
-            val tr = Toplevel.exec_id exec_id command;
-            val opt_context = try Toplevel.generic_theory_of st';
-          in
-            if failed andalso strict then ()
-            else print_error tr opt_context (fn () => print_fn tr st')
-          end;
-      in
-        Print {
-          name = name, args = args, delay = delay, pri = pri, persistent = persistent,
-          exec_id = exec_id, print_process = Lazy.lazy_name "Command.print" process}
-      end;
-
-    fun bad_print name args exn =
-      make_print name args {delay = NONE, pri = 0, persistent = false,
-        strict = false, print_fn = fn _ => fn _ => Exn.reraise exn};
-
-    fun new_print name args get_pr =
+    fun new_print (name, args) get_pr =
       let
         val params =
          {keywords = keywords,
@@ -355,31 +360,36 @@
       in
         (case Exn.capture (Runtime.controlled_execution NONE get_pr) params of
           Exn.Res NONE => NONE
-        | Exn.Res (SOME pr) => SOME (make_print name args pr)
-        | Exn.Exn exn => SOME (bad_print name args exn))
+        | Exn.Res (SOME pr) => SOME (make_print (name, args) pr eval)
+        | Exn.Exn exn => SOME (bad_print (name, args) exn eval))
       end;
 
-    fun get_print (a, b) =
-      (case find_first (fn Print {name, args, ...} => name = a andalso args = b) old_prints of
+    fun get_print (name, args) =
+      (case find_first (fn Print print => (#name print, #args print) = (name, args)) old_prints of
         NONE =>
-          (case AList.lookup (op =) print_functions a of
-            NONE => SOME (bad_print a b (ERROR ("Missing print function " ^ quote a)))
-          | SOME get_pr => new_print a b get_pr)
+          (case AList.lookup (op =) print_functions name of
+            NONE =>
+              SOME (bad_print (name, args) (ERROR ("Missing print function " ^ quote name)) eval)
+          | SOME get_pr => new_print (name, args) get_pr)
       | some => some);
 
-    val new_prints =
+    val retained_prints =
+      filter (fn print => print_finished print andalso print_persistent print) old_prints;
+    val visible_prints =
       if command_visible then
-        fold (fn (a, _) => cons (a, [])) print_functions command_overlays
+        fold (fn (name, _) => cons (name, [])) print_functions command_overlays
         |> sort_distinct overlay_ord
         |> map_filter get_print
-      else filter (fn print => print_finished print andalso print_persistent print) old_prints;
+      else [];
+    val new_prints = visible_prints @ retained_prints;
   in
     if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints
   end;
 
 fun print_function name f =
   Synchronized.change print_functions (fn funs =>
-   (if not (AList.defined (op =) funs name) then ()
+   (if name = "" then error "Unnamed print function" else ();
+    if not (AList.defined (op =) funs name) then ()
     else warning ("Redefining command print function: " ^ quote name);
     AList.update (op =) (name, f) funs));
 
diff -r 9946707cf329 -r 3f60cba346aa src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Thu May 31 10:59:54 2018 +0200
+++ b/src/Pure/PIDE/command.scala	Thu May 31 22:59:08 2018 +0200
@@ -261,9 +261,7 @@
     markups: Markups = Markups.empty)
   {
     def initialized: Boolean = status.exists(markup => markup.name == Markup.INITIALIZED)
-
-    lazy val consolidated: Boolean =
-      status.exists(markup => markup.name == Markup.CONSOLIDATED)
+    def consolidated: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATED)
 
     lazy val protocol_status: Protocol.Status =
     {
diff -r 9946707cf329 -r 3f60cba346aa src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Thu May 31 10:59:54 2018 +0200
+++ b/src/Pure/PIDE/document.ML	Thu May 31 22:59:08 2018 +0200
@@ -24,8 +24,7 @@
   val command_exec: state -> string -> Document_ID.command -> Command.exec option
   val remove_versions: Document_ID.version list -> state -> state
   val start_execution: state -> state
-  val consolidate_execution: state -> unit
-  val update: Document_ID.version -> Document_ID.version -> edit list -> state ->
+  val update: Document_ID.version -> Document_ID.version -> edit list -> bool -> state ->
     Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state
   val state: unit -> state
   val change_state: (state -> state) -> unit
@@ -55,24 +54,22 @@
 
 structure Entries = Linear_Set(type key = Document_ID.command val ord = int_ord);
 
-type consolidation = (int -> int option) * Thy_Output.segment list;
-
 abstype node = Node of
  {header: node_header,  (*master directory, theory header, errors*)
   keywords: Keyword.keywords option,  (*outer syntax keywords*)
   perspective: perspective,  (*command perspective*)
   entries: Command.exec option Entries.T,  (*command entries with executions*)
-  result: Command.eval option,  (*result of last execution*)
-  consolidation: consolidation future}  (*consolidation status of eval forks*)
+  result: (Document_ID.command * Command.eval) option,  (*result of last execution*)
+  consolidated: unit lazy}  (*consolidated status of eval forks*)
 and version = Version of node String_Graph.T  (*development graph wrt. static imports*)
 with
 
-fun make_node (header, keywords, perspective, entries, result, consolidation) =
+fun make_node (header, keywords, perspective, entries, result, consolidated) =
   Node {header = header, keywords = keywords, perspective = perspective,
-    entries = entries, result = result, consolidation = consolidation};
+    entries = entries, result = result, consolidated = consolidated};
 
-fun map_node f (Node {header, keywords, perspective, entries, result, consolidation}) =
-  make_node (f (header, keywords, perspective, entries, result, consolidation));
+fun map_node f (Node {header, keywords, perspective, entries, result, consolidated}) =
+  make_node (f (header, keywords, perspective, entries, result, consolidated));
 
 fun make_perspective (required, command_ids, overlays) : perspective =
  {required = required,
@@ -85,7 +82,7 @@
 val no_perspective = make_perspective (false, [], []);
 
 val empty_node =
-  make_node (no_header, NONE, no_perspective, Entries.empty, NONE, Future.value (K NONE, []));
+  make_node (no_header, NONE, no_perspective, Entries.empty, NONE, Lazy.value ());
 
 fun is_no_perspective ({required, visible, visible_last, overlays}: perspective) =
   not required andalso
@@ -93,13 +90,13 @@
   is_none visible_last andalso
   Inttab.is_empty overlays;
 
-fun is_empty_node (Node {header, keywords, perspective, entries, result, consolidation}) =
+fun is_empty_node (Node {header, keywords, perspective, entries, result, consolidated}) =
   header = no_header andalso
   is_none keywords andalso
   is_no_perspective perspective andalso
   Entries.is_empty entries andalso
   is_none result andalso
-  Future.is_finished consolidation;
+  Lazy.is_finished consolidated;
 
 
 (* basic components *)
@@ -110,15 +107,15 @@
   | _ => Path.current);
 
 fun set_header master header errors =
-  map_node (fn (_, keywords, perspective, entries, result, consolidation) =>
+  map_node (fn (_, keywords, perspective, entries, result, consolidated) =>
     ({master = master, header = header, errors = errors},
-      keywords, perspective, entries, result, consolidation));
+      keywords, perspective, entries, result, consolidated));
 
 fun get_header (Node {header, ...}) = header;
 
 fun set_keywords keywords =
-  map_node (fn (header, _, perspective, entries, result, consolidation) =>
-    (header, keywords, perspective, entries, result, consolidation));
+  map_node (fn (header, _, perspective, entries, result, consolidated) =>
+    (header, keywords, perspective, entries, result, consolidated));
 
 fun get_keywords (Node {keywords, ...}) = keywords;
 
@@ -142,8 +139,8 @@
 fun get_perspective (Node {perspective, ...}) = perspective;
 
 fun set_perspective args =
-  map_node (fn (header, keywords, _, entries, result, consolidation) =>
-    (header, keywords, make_perspective args, entries, result, consolidation));
+  map_node (fn (header, keywords, _, entries, result, consolidated) =>
+    (header, keywords, make_perspective args, entries, result, consolidated));
 
 val required_node = #required o get_perspective;
 val visible_command = Inttab.defined o #visible o get_perspective;
@@ -152,8 +149,8 @@
 val overlays = Inttab.lookup_list o #overlays o get_perspective;
 
 fun map_entries f =
-  map_node (fn (header, keywords, perspective, entries, result, consolidation) =>
-    (header, keywords, perspective, f entries, result, consolidation));
+  map_node (fn (header, keywords, perspective, entries, result, consolidated) =>
+    (header, keywords, perspective, f entries, result, consolidated));
 
 fun get_entries (Node {entries, ...}) = entries;
 
@@ -166,30 +163,40 @@
 fun get_result (Node {result, ...}) = result;
 
 fun set_result result =
-  map_node (fn (header, keywords, perspective, entries, _, consolidation) =>
-    (header, keywords, perspective, entries, result, consolidation));
+  map_node (fn (header, keywords, perspective, entries, _, consolidated) =>
+    (header, keywords, perspective, entries, result, consolidated));
 
 fun pending_result node =
   (case get_result node of
-    SOME eval => not (Command.eval_finished eval)
+    SOME (_, eval) => not (Command.eval_finished eval)
   | NONE => false);
 
 fun finished_result node =
   (case get_result node of
-    SOME eval => Command.eval_finished eval
+    SOME (_, eval) => Command.eval_finished eval
   | NONE => false);
 
 fun finished_result_theory node =
   if finished_result node then
-    let val st = Command.eval_result_state (the (get_result node))
-    in SOME (Toplevel.end_theory Position.none st) handle ERROR _ => NONE end
+    let
+      val (result_id, eval) = the (get_result node);
+      val st = Command.eval_result_state eval;
+    in SOME (result_id, Toplevel.end_theory Position.none st) handle ERROR _ => NONE end
   else NONE;
 
-val reset_consolidation =
+val reset_consolidated =
   map_node (fn (header, keywords, perspective, entries, result, _) =>
-    (header, keywords, perspective, entries, result, Future.promise I));
+    (header, keywords, perspective, entries, result, Lazy.lazy I));
+
+fun get_consolidated (Node {consolidated, ...}) = consolidated;
+
+val is_consolidated = Lazy.is_finished o get_consolidated;
 
-fun get_consolidation (Node {consolidation, ...}) = consolidation;
+fun commit_consolidated node =
+  (Lazy.force (get_consolidated node); Output.status (Markup.markup_only Markup.consolidated));
+
+fun could_consolidate node =
+  not (is_consolidated node) andalso is_some (finished_result_theory node);
 
 fun get_node nodes name = String_Graph.get_node nodes name
   handle String_Graph.UNDEF _ => empty_node;
@@ -414,9 +421,6 @@
 
 val the_command_name = #1 oo the_command;
 
-fun force_command_span state =
-  Outer_Syntax.make_span o Lazy.force o #4 o the_command state;
-
 
 (* execution *)
 
@@ -515,77 +519,6 @@
         {version_id = version_id, execution_id = execution_id, delay_request = delay_request'};
     in (versions, blobs, commands, execution') end));
 
-fun presentation options thy node_name node =
-  if Options.bool options "editor_presentation" then
-    let
-      val (adjust, segments) = Future.get_finished (get_consolidation node);
-      val presentation_context: Thy_Info.presentation_context =
-       {options = options,
-        file_pos = Position.file node_name,
-        adjust_pos = Position.adjust_offsets adjust,
-        segments = segments};
-    in Thy_Info.apply_presentation presentation_context thy end
-  else ();
-
-fun consolidate_execution state =
-  let
-    fun check_consolidation node_name node =
-      if Future.is_finished (get_consolidation node) then ()
-      else
-        (case finished_result_theory node of
-          NONE => ()
-        | SOME thy =>
-            let
-              val result_id = Command.eval_exec_id (the (get_result node));
-              val eval_ids =
-                iterate_entries (fn (_, opt_exec) => fn eval_ids =>
-                  (case opt_exec of
-                    SOME (eval, _) => SOME (cons (Command.eval_exec_id eval) eval_ids)
-                  | NONE => NONE)) node [];
-            in
-              (case Execution.snapshot eval_ids of
-                [] =>
-                  let
-                    val (_, offsets, rev_segments) =
-                      iterate_entries (fn (_, opt_exec) => fn (offset, offsets, segments) =>
-                        (case opt_exec of
-                          SOME (eval, _) =>
-                            let
-                              val command_id = Command.eval_command_id eval;
-                              val span = force_command_span state command_id;
-
-                              val exec_id = Command.eval_exec_id eval;
-                              val tr = Command.eval_result_command eval;
-                              val st' = Command.eval_result_state eval;
-
-                              val offset' = offset + the_default 0 (Command_Span.symbol_length span);
-                              val offsets' = offsets
-                                |> Inttab.update (command_id, offset)
-                                |> Inttab.update (exec_id, offset);
-                              val segments' = (span, tr, st') :: segments;
-                            in SOME (offset', offsets', segments') end
-                        | NONE => NONE)) node (0, Inttab.empty, []);
-
-                    val adjust = Inttab.lookup offsets;
-                    val segments =
-                      rev rev_segments |> map (fn (span, tr, st') =>
-                        {span = Command_Span.adjust_offsets adjust span, command = tr, state = st'});
-
-                    val _ = Future.fulfill (get_consolidation node) (adjust, segments);
-                    val _ =
-                      Position.setmp_thread_data (Position.id_only (Document_ID.print result_id))
-                        (fn () =>
-                          (Output.status (Markup.markup_only Markup.consolidated);
-                            (* FIXME avoid user operations on protocol thread *)
-                            presentation (Options.default ()) thy node_name node)) ();
-                  in () end
-              | _ => ())
-            end);
-      in
-        String_Graph.fold (fn (node_name, (node, _)) => fn () => check_consolidation node_name node)
-          (nodes_of (get_execution_version state)) ()
-      end;
-
 
 
 (** document update **)
@@ -596,6 +529,7 @@
 
 val assign_update_empty: assign_update = Inttab.empty;
 fun assign_update_defined (tab: assign_update) command_id = Inttab.defined tab command_id;
+fun assign_update_change entry (tab: assign_update) = Inttab.update entry tab;
 fun assign_update_apply (tab: assign_update) node = Inttab.fold assign_entry tab node;
 
 fun assign_update_new upd (tab: assign_update) =
@@ -626,7 +560,7 @@
             maybe_end_theory pos
               (case get_result (snd (the (AList.lookup (op =) deps import))) of
                 NONE => Toplevel.toplevel
-              | SOME eval => Command.eval_result_state eval)
+              | SOME (_, eval) => Command.eval_result_state eval)
         | some => some)
         |> Option.map (fn thy => (thy, (pos, Theory.get_markup thy))));
 
@@ -727,10 +661,78 @@
 fun removed_execs node0 (command_id, exec_ids) =
   subtract (op =) exec_ids (Command.exec_ids (lookup_entry node0 command_id));
 
+fun print_consolidation options the_command_span node_name (assign_update, node) =
+  (case finished_result_theory node of
+    SOME (result_id, thy) =>
+      let
+        val eval_ids =
+          iterate_entries (fn (_, opt_exec) => fn eval_ids =>
+            (case opt_exec of
+              SOME (eval, _) => SOME (cons (Command.eval_exec_id eval) eval_ids)
+            | NONE => NONE)) node [];
+      in
+        if null (Execution.snapshot eval_ids) then
+          let
+            val consolidation =
+              if Options.bool options "editor_presentation" then
+                let
+                  val (_, offsets, rev_segments) =
+                    iterate_entries (fn (_, opt_exec) => fn (offset, offsets, segments) =>
+                      (case opt_exec of
+                        SOME (eval, _) =>
+                          let
+                            val command_id = Command.eval_command_id eval;
+                            val span = the_command_span command_id;
+
+                            val exec_id = Command.eval_exec_id eval;
+                            val tr = Command.eval_result_command eval;
+                            val st' = Command.eval_result_state eval;
+
+                            val offset' = offset + the_default 0 (Command_Span.symbol_length span);
+                            val offsets' = offsets
+                              |> Inttab.update (command_id, offset)
+                              |> Inttab.update (exec_id, offset);
+                            val segments' = (span, tr, st') :: segments;
+                          in SOME (offset', offsets', segments') end
+                      | NONE => NONE)) node (0, Inttab.empty, []);
+
+                  val adjust = Inttab.lookup offsets;
+                  val segments =
+                    rev rev_segments |> map (fn (span, tr, st') =>
+                      {span = Command_Span.adjust_offsets adjust span, command = tr, state = st'});
+
+                  val presentation_context: Thy_Info.presentation_context =
+                   {options = options,
+                    file_pos = Position.file node_name,
+                    adjust_pos = Position.adjust_offsets adjust,
+                    segments = segments};
+                in
+                  fn () =>
+                    (Thy_Info.apply_presentation presentation_context thy;
+                     commit_consolidated node)
+                end
+              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)));
+
+            val assign_update' = assign_update |> assign_update_change result_entry;
+            val node' = node |> assign_entry result_entry;
+          in (assign_update', node') end
+        else (assign_update, node)
+      end
+  | NONE => (assign_update, node));
 in
 
-fun update old_version_id new_version_id edits state = Runtime.exn_trace_system (fn () =>
+fun update old_version_id new_version_id edits consolidate state =
+  Runtime.exn_trace_system (fn () =>
   let
+    val options = Options.default ();
+    val the_command_span = Outer_Syntax.make_span o Lazy.force o #4 o the_command state;
+
     val old_version = the_version state old_version_id;
     val new_version =
       timeit "Document.edit_nodes"
@@ -753,12 +755,15 @@
                   let
                     val root_theory = check_root_theory node;
                     val keywords = the_default (Session.get_keywords ()) (get_keywords node);
+
+                    val maybe_consolidate = consolidate andalso could_consolidate node;
                     val imports = map (apsnd Future.join) deps;
                     val imports_result_changed = exists (#4 o #1 o #2) imports;
                     val node_required = Symtab.defined required name;
                   in
-                    if Symtab.defined edited name orelse visible_node node orelse
-                      imports_result_changed orelse Symtab.defined required0 name <> node_required
+                    if Symtab.defined edited name orelse maybe_consolidate orelse
+                      visible_node node orelse imports_result_changed orelse
+                      Symtab.defined required0 name <> node_required
                     then
                       let
                         val node0 = node_of old_version name;
@@ -785,7 +790,7 @@
                                 if not node_required andalso prev = visible_last node then NONE
                                 else new_exec keywords state node proper_init id res) node;
 
-                        val assigned_execs =
+                        val assign_update =
                           (node0, updated_execs) |-> iterate_entries_after common
                             (fn ((_, command_id0), exec0) => fn res =>
                               if is_none exec0 then NONE
@@ -796,32 +801,36 @@
                           if command_id' = Document_ID.none then NONE else SOME command_id';
                         val result =
                           if is_none last_exec orelse is_some (after_entry node last_exec) then NONE
-                          else SOME (#1 exec');
-
-                        val assign_update = assign_update_result assigned_execs;
-                        val removed = maps (removed_execs node0) assign_update;
-                        val _ = List.app Execution.cancel removed;
+                          else SOME (command_id', #1 exec');
 
                         val result_changed =
-                          not (eq_option Command.eval_eq (get_result node0, result));
-                        val node' = node
-                          |> assign_update_apply assigned_execs
+                          not (eq_option (Command.eval_eq o apply2 #2) (get_result node0, result));
+                        val (assign_update', node') = node
+                          |> assign_update_apply assign_update
                           |> set_result result
-                          |> result_changed ? reset_consolidation;
+                          |> result_changed ? reset_consolidated
+                          |> pair assign_update
+                          |> (not result_changed andalso maybe_consolidate) ?
+                              print_consolidation options the_command_span name;
+
+                        val assign_result = assign_update_result assign_update';
+                        val removed = maps (removed_execs node0) assign_result;
+                        val _ = List.app Execution.cancel removed;
+
                         val assigned_node = SOME (name, node');
-                      in ((removed, assign_update, assigned_node, result_changed), node') end
+                      in ((removed, assign_result, assigned_node, result_changed), node') end
                     else (([], [], NONE, false), node)
                   end))))
       |> Future.joins |> map #1);
 
     val removed = maps #1 updated;
-    val assign_update = maps #2 updated;
+    val assign_result = maps #2 updated;
     val assigned_nodes = map_filter #3 updated;
 
     val state' = state
       |> define_version new_version_id (fold put_node assigned_nodes new_version);
 
-  in (removed, assign_update, state') end);
+  in (removed, assign_result, state') end);
 
 end;
 
diff -r 9946707cf329 -r 3f60cba346aa src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu May 31 10:59:54 2018 +0200
+++ b/src/Pure/PIDE/document.scala	Thu May 31 22:59:08 2018 +0200
@@ -930,8 +930,10 @@
 
     def node_consolidated(version: Version, name: Node.Name): Boolean =
       !name.is_theory ||
-        version.nodes(name).commands.reverse.iterator.
-          flatMap(command_states(version, _)).exists(_.consolidated)
+      {
+        val it = version.nodes(name).commands.reverse.iterator
+        it.hasNext && command_states(version, it.next).exists(_.consolidated)
+      }
 
     // persistent user-view
     def snapshot(name: Node.Name = Node.Name.empty, pending_edits: List[Text.Edit] = Nil)
diff -r 9946707cf329 -r 3f60cba346aa src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Thu May 31 10:59:54 2018 +0200
+++ b/src/Pure/PIDE/protocol.ML	Thu May 31 22:59:08 2018 +0200
@@ -64,10 +64,6 @@
       end);
 
 val _ =
-  Isabelle_Process.protocol_command "Document.consolidate_execution"
-    (fn [] => Document.consolidate_execution (Document.state ()));
-
-val _ =
   Isabelle_Process.protocol_command "Document.discontinue_execution"
     (fn [] => Execution.discontinue ());
 
@@ -78,49 +74,52 @@
 val _ =
   Isabelle_Process.protocol_command "Document.update"
     (Future.task_context "Document.update" (Future.new_group NONE)
-      (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
-        let
-          val _ = Execution.discontinue ();
+      (fn [old_id_string, new_id_string, edits_yxml, consolidate_string] =>
+        Document.change_state (fn state =>
+          let
+            val old_id = Document_ID.parse old_id_string;
+            val new_id = Document_ID.parse new_id_string;
+            val edits =
+              YXML.parse_body edits_yxml |>
+                let open XML.Decode in
+                  list (pair string
+                    (variant
+                     [fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
+                      fn ([], a) =>
+                        let
+                          val (master, (name, (imports, (keywords, errors)))) =
+                            pair string (pair string (pair (list string)
+                              (pair (list (pair string
+                                (pair (pair string (list string)) (list string))))
+                                (list YXML.string_of_body)))) a;
+                          val imports' = map (rpair Position.none) imports;
+                          val keywords' = map (fn (x, y) => ((x, Position.none), y)) keywords;
+                          val header = Thy_Header.make (name, Position.none) imports' keywords';
+                        in Document.Deps {master = master, header = header, errors = errors} end,
+                      fn (a :: b, c) =>
+                        Document.Perspective (bool_atom a, map int_atom b,
+                          list (pair int (pair string (list string))) c)]))
+                end;
+            val consolidate = Value.parse_bool consolidate_string;
 
-          val old_id = Document_ID.parse old_id_string;
-          val new_id = Document_ID.parse new_id_string;
-          val edits =
-            YXML.parse_body edits_yxml |>
-              let open XML.Decode in
-                list (pair string
-                  (variant
-                   [fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
-                    fn ([], a) =>
-                      let
-                        val (master, (name, (imports, (keywords, errors)))) =
-                          pair string (pair string (pair (list string)
-                            (pair (list (pair string
-                              (pair (pair string (list string)) (list string))))
-                              (list YXML.string_of_body)))) a;
-                        val imports' = map (rpair Position.none) imports;
-                        val keywords' = map (fn (x, y) => ((x, Position.none), y)) keywords;
-                        val header = Thy_Header.make (name, Position.none) imports' keywords';
-                      in Document.Deps {master = master, header = header, errors = errors} end,
-                    fn (a :: b, c) =>
-                      Document.Perspective (bool_atom a, map int_atom b,
-                        list (pair int (pair string (list string))) c)]))
-              end;
+            val _ = Execution.discontinue ();
 
-          val (removed, assign_update, state') = Document.update old_id new_id edits state;
-          val _ =
-            (singleton o Future.forks)
-             {name = "Document.update/remove", group = NONE,
-              deps = Execution.snapshot removed,
-              pri = Task_Queue.urgent_pri + 2, interrupts = false}
-             (fn () => (Execution.purge removed; List.app Isabelle_Process.reset_tracing removed));
+            val (removed, assign_update, state') =
+              Document.update old_id new_id edits consolidate state;
+            val _ =
+              (singleton o Future.forks)
+               {name = "Document.update/remove", group = NONE,
+                deps = Execution.snapshot removed,
+                pri = Task_Queue.urgent_pri + 2, interrupts = false}
+               (fn () => (Execution.purge removed; List.app Isabelle_Process.reset_tracing removed));
 
-          val _ =
-            Output.protocol_message Markup.assign_update
-              [(new_id, assign_update) |>
-                let open XML.Encode
-                in pair int (list (pair int (list int))) end
-                |> YXML.string_of_body];
-        in Document.start_execution state' end)));
+            val _ =
+              Output.protocol_message Markup.assign_update
+                [(new_id, assign_update) |>
+                  let open XML.Encode
+                  in pair int (list (pair int (list int))) end
+                  |> YXML.string_of_body];
+          in Document.start_execution state' end)));
 
 val _ =
   Isabelle_Process.protocol_command "Document.remove_versions"
diff -r 9946707cf329 -r 3f60cba346aa src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Thu May 31 10:59:54 2018 +0200
+++ b/src/Pure/PIDE/protocol.scala	Thu May 31 22:59:08 2018 +0200
@@ -409,9 +409,6 @@
 
   /* execution */
 
-  def consolidate_execution(): Unit =
-    protocol_command("Document.consolidate_execution")
-
   def discontinue_execution(): Unit =
     protocol_command("Document.discontinue_execution")
 
@@ -422,7 +419,7 @@
   /* document versions */
 
   def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
-    edits: List[Document.Edit_Command])
+    edits: List[Document.Edit_Command], consolidate: Boolean)
   {
     val edits_yxml =
     {
@@ -450,7 +447,8 @@
         pair(string, encode_edit(name))(name.node, edit)
       })
       Symbol.encode_yxml(encode_edits(edits)) }
-    protocol_command("Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml)
+    protocol_command(
+      "Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml, consolidate.toString)
   }
 
   def remove_versions(versions: List[Document.Version])
diff -r 9946707cf329 -r 3f60cba346aa src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Thu May 31 10:59:54 2018 +0200
+++ b/src/Pure/PIDE/resources.scala	Thu May 31 22:59:08 2018 +0200
@@ -215,8 +215,9 @@
       reparse_limit: Int,
       previous: Document.Version,
       doc_blobs: Document.Blobs,
-      edits: List[Document.Edit_Text]): Session.Change =
-    Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits)
+      edits: List[Document.Edit_Text],
+      consolidate: Boolean): Session.Change =
+    Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits, consolidate)
 
   def commit(change: Session.Change) { }
 
diff -r 9946707cf329 -r 3f60cba346aa src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Thu May 31 10:59:54 2018 +0200
+++ b/src/Pure/PIDE/session.scala	Thu May 31 22:59:08 2018 +0200
@@ -50,6 +50,7 @@
     syntax_changed: List[Document.Node.Name],
     deps_changed: Boolean,
     doc_edits: List[Document.Edit_Command],
+    consolidate: Boolean,
     version: Document.Version)
 
   case object Change_Flush
@@ -230,15 +231,16 @@
     previous: Future[Document.Version],
     doc_blobs: Document.Blobs,
     text_edits: List[Document.Edit_Text],
+    consolidate: Boolean,
     version_result: Promise[Document.Version])
 
   private val change_parser = Consumer_Thread.fork[Text_Edits]("change_parser", daemon = true)
   {
-    case Text_Edits(previous, doc_blobs, text_edits, version_result) =>
+    case Text_Edits(previous, doc_blobs, text_edits, consolidate, version_result) =>
       val prev = previous.get_finished
       val change =
         Timing.timeit("parse_change", timing) {
-          resources.parse_change(reparse_limit, prev, doc_blobs, text_edits)
+          resources.parse_change(reparse_limit, prev, doc_blobs, text_edits, consolidate)
         }
       version_result.fulfill(change.version)
       manager.send(change)
@@ -342,7 +344,10 @@
   {
     /* raw edits */
 
-    def handle_raw_edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
+    def handle_raw_edits(
+      doc_blobs: Document.Blobs = Document.Blobs.empty,
+      edits: List[Document.Edit_Text] = Nil,
+      consolidate: Boolean = false)
     //{{{
     {
       require(prover.defined)
@@ -354,7 +359,7 @@
       global_state.change(_.continue_history(previous, edits, version))
 
       raw_edits.post(Session.Raw_Edits(doc_blobs, edits))
-      change_parser.send(Text_Edits(previous, doc_blobs, edits, version))
+      change_parser.send(Text_Edits(previous, doc_blobs, edits, consolidate, version))
     }
     //}}}
 
@@ -392,7 +397,7 @@
 
       val assignment = global_state.value.the_assignment(change.previous).check_finished
       global_state.change(_.define_version(change.version, assignment))
-      prover.get.update(change.previous.id, change.version.id, change.doc_edits)
+      prover.get.update(change.previous.id, change.version.id, change.doc_edits, change.consolidate)
       resources.commit(change)
     }
     //}}}
@@ -529,7 +534,7 @@
             }
 
           case Consolidate_Execution =>
-            if (prover.defined) prover.get.consolidate_execution()
+            if (prover.defined) handle_raw_edits(consolidate = true)
 
           case Prune_History =>
             if (prover.defined) {
@@ -540,7 +545,7 @@
           case Update_Options(options) =>
             if (prover.defined && is_ready) {
               prover.get.options(options)
-              handle_raw_edits(Document.Blobs.empty, Nil)
+              handle_raw_edits()
             }
             global_options.post(Session.Global_Options(options))
 
@@ -548,7 +553,7 @@
             prover.get.cancel_exec(exec_id)
 
           case Session.Raw_Edits(doc_blobs, edits) if prover.defined =>
-            handle_raw_edits(doc_blobs, edits)
+            handle_raw_edits(doc_blobs = doc_blobs, edits = edits)
 
           case Session.Dialog_Result(id, serial, result) if prover.defined =>
             prover.get.dialog_result(serial, result)
diff -r 9946707cf329 -r 3f60cba346aa src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Thu May 31 10:59:54 2018 +0200
+++ b/src/Pure/System/progress.scala	Thu May 31 22:59:08 2018 +0200
@@ -51,7 +51,10 @@
   }
 
   override def theory(session: String, theory: String): Unit =
-    if (verbose) echo(session + ": theory " + theory)
+    if (verbose) {
+      if (session == "") echo("theory " + theory)
+      else echo(session + ": theory " + theory)
+    }
 
   @volatile private var is_stopped = false
   override def interrupt_handler[A](e: => A): A =
diff -r 9946707cf329 -r 3f60cba346aa src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Thu May 31 10:59:54 2018 +0200
+++ b/src/Pure/Thy/export.scala	Thu May 31 22:59:08 2018 +0200
@@ -288,8 +288,10 @@
 
     if (!no_build) {
       val rc =
-        Build.build_logic(options, session_name, progress = progress,
-          dirs = dirs, system_mode = system_mode)
+        progress.interrupt_handler {
+          Build.build_logic(options, session_name, progress = progress,
+            dirs = dirs, system_mode = system_mode)
+        }
       if (rc != 0) sys.exit(rc)
     }
 
diff -r 9946707cf329 -r 3f60cba346aa src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Thu May 31 10:59:54 2018 +0200
+++ b/src/Pure/Thy/thy_resources.scala	Thu May 31 22:59:08 2018 +0200
@@ -144,9 +144,32 @@
         Event_Timer.request(Time.now(), repeat = Some(Time.seconds(0.5)))
           { if (progress.stopped) result.cancel else check_state }
 
+      val theories_progress = Synchronized(Set.empty[Document.Node.Name])
+
       val consumer =
         Session.Consumer[Session.Commands_Changed](getClass.getName) {
-          case changed => if (dep_theories.exists(changed.nodes)) check_state
+          case changed =>
+            if (dep_theories.exists(changed.nodes)) {
+
+              val check_theories =
+                (for (command <- changed.commands.iterator if command.potentially_initialized)
+                  yield command.node_name).toSet
+
+              if (check_theories.nonEmpty) {
+                val snapshot = session.snapshot()
+                val initialized =
+                  theories_progress.change_result(theories =>
+                  {
+                    val initialized =
+                      (check_theories -- theories).toList.filter(name =>
+                        Protocol.node_status(snapshot.state, snapshot.version, name).initialized)
+                    (initialized, theories ++ initialized)
+                  })
+                initialized.map(_.theory).sorted.foreach(progress.theory("", _))
+              }
+
+              check_state
+            }
         }
 
       try {
diff -r 9946707cf329 -r 3f60cba346aa src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Thu May 31 10:59:54 2018 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Thu May 31 22:59:08 2018 +0200
@@ -296,7 +296,8 @@
       reparse_limit: Int,
       previous: Document.Version,
       doc_blobs: Document.Blobs,
-      edits: List[Document.Edit_Text]): Session.Change =
+      edits: List[Document.Edit_Text],
+      consolidate: Boolean): Session.Change =
   {
     val (syntax_changed, nodes0, doc_edits0) = header_edits(resources, previous, edits)
 
@@ -356,6 +357,7 @@
         (doc_edits.toList.filterNot(_._2.is_void), Document.Version.make(nodes))
       }
 
-    Session.Change(previous, syntax_changed, syntax_changed.nonEmpty, doc_edits, version)
+    Session.Change(
+      previous, syntax_changed, syntax_changed.nonEmpty, doc_edits, consolidate, version)
   }
 }
diff -r 9946707cf329 -r 3f60cba346aa src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu May 31 10:59:54 2018 +0200
+++ b/src/Pure/Tools/build.scala	Thu May 31 22:59:08 2018 +0200
@@ -836,10 +836,8 @@
         system_mode = system_mode, sessions = List(logic)).ok) 0
     else {
       progress.echo("Build started for Isabelle/" + logic + " ...")
-      progress.interrupt_handler {
-        Build.build(options, progress = progress, build_heap = build_heap, dirs = dirs,
-          system_mode = system_mode, sessions = List(logic)).rc
-      }
+      Build.build(options, progress = progress, build_heap = build_heap, dirs = dirs,
+        system_mode = system_mode, sessions = List(logic)).rc
     }
   }
 }
diff -r 9946707cf329 -r 3f60cba346aa src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Thu May 31 10:59:54 2018 +0200
+++ b/src/Pure/Tools/dump.scala	Thu May 31 22:59:08 2018 +0200
@@ -21,32 +21,28 @@
       Bytes.write(path, bytes)
     }
 
-    def write(node_name: Document.Node.Name, file_name: String, text: String)
-    {
+    def write(node_name: Document.Node.Name, file_name: String, text: String): Unit =
       write(node_name, file_name, Bytes(text))
-    }
+
+    def write(node_name: Document.Node.Name, file_name: String, body: XML.Body): Unit =
+      write(node_name, file_name, Symbol.encode(YXML.string_of_body(body)))
   }
 
   sealed case class Aspect(name: String, description: String, operation: Aspect_Args => Unit)
 
   private val known_aspects =
     List(
-      Aspect("list", "list theory nodes",
-        { case args =>
-            for (node_name <- args.result.node_names) args.progress.echo(node_name.toString)
-        }),
       Aspect("messages", "output messages (YXML format)",
         { case args =>
             for (node_name <- args.result.node_names) {
               args.write(node_name, "messages.yxml",
-                YXML.string_of_body(args.result.messages(node_name).iterator.map(_._1).toList))
+                args.result.messages(node_name).iterator.map(_._1).toList)
             }
         }),
       Aspect("markup", "PIDE markup (YXML format)",
         { case args =>
             for (node_name <- args.result.node_names) {
-              args.write(node_name, "markup.yxml",
-                YXML.string_of_body(args.result.markup_to_XML(node_name)))
+              args.write(node_name, "markup.yxml", args.result.markup_to_XML(node_name))
             }
         })
     )
@@ -176,21 +172,23 @@
       val progress = new Console_Progress(verbose = verbose)
 
       val result =
-        dump(options, logic,
-          aspects = aspects,
-          progress = progress,
-          dirs = dirs,
-          select_dirs = select_dirs,
-          output_dir = output_dir,
-          verbose = verbose,
-          selection = Sessions.Selection(
-            requirements = requirements,
-            all_sessions = all_sessions,
-            base_sessions = base_sessions,
-            exclude_session_groups = exclude_session_groups,
-            exclude_sessions = exclude_sessions,
-            session_groups = session_groups,
-            sessions = sessions))
+        progress.interrupt_handler {
+          dump(options, logic,
+            aspects = aspects,
+            progress = progress,
+            dirs = dirs,
+            select_dirs = select_dirs,
+            output_dir = output_dir,
+            verbose = verbose,
+            selection = Sessions.Selection(
+              requirements = requirements,
+              all_sessions = all_sessions,
+              base_sessions = base_sessions,
+              exclude_session_groups = exclude_session_groups,
+              exclude_sessions = exclude_sessions,
+              session_groups = session_groups,
+              sessions = sessions))
+        }
 
       progress.echo(result.timing.message_resources)