maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);

--- a/etc/options	Tue Aug 08 12:21:29 2017 +0200
+++ b/etc/options	Tue Aug 08 22:13:05 2017 +0200
@@ -155,6 +155,9 @@
 public option editor_output_delay : real = 0.1
   -- "delay for prover output (markup, common messages etc.)"
 
+public option editor_consolidate_delay : real = 1.0
+  -- "delay to consolidate status of command evaluation (execution forks)"
+
 public option editor_prune_delay : real = 15
   -- "delay to prune history (delete old versions)"
 

--- a/src/Pure/PIDE/command.ML	Tue Aug 08 12:21:29 2017 +0200
+++ b/src/Pure/PIDE/command.ML	Tue Aug 08 22:13:05 2017 +0200
@@ -12,6 +12,7 @@
   val read: Keyword.keywords -> theory -> Path.T-> (unit -> theory) ->
     blob list * int -> Token.T list -> Toplevel.transition
   type eval
+  val eval_exec_id: eval -> Document_ID.exec
   val eval_eq: eval * eval -> bool
   val eval_running: eval -> bool
   val eval_finished: eval -> bool

--- a/src/Pure/PIDE/command.scala	Tue Aug 08 12:21:29 2017 +0200
+++ b/src/Pure/PIDE/command.scala	Tue Aug 08 22:13:05 2017 +0200
@@ -213,6 +213,9 @@
     results: Results = Results.empty,
     markups: Markups = Markups.empty)
   {
+    lazy val consolidated: Boolean =
+      status.exists(markup => markup.name == Markup.CONSOLIDATED)
+
     lazy val protocol_status: Protocol.Status =
     {
       val warnings =

--- a/src/Pure/PIDE/document.ML	Tue Aug 08 12:21:29 2017 +0200
+++ b/src/Pure/PIDE/document.ML	Tue Aug 08 22:13:05 2017 +0200
@@ -24,6 +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 ->
     Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state
   val state: unit -> state
@@ -59,16 +60,17 @@
   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*)
+  result: Command.eval option,  (*result of last execution*)
+  consolidated: unit lazy}  (*consolidation 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) =
+fun make_node (header, keywords, perspective, entries, result, consolidated) =
   Node {header = header, keywords = keywords, perspective = perspective,
-    entries = entries, result = result};
+    entries = entries, result = result, consolidated = consolidated};
 
-fun map_node f (Node {header, keywords, perspective, entries, result}) =
-  make_node (f (header, keywords, perspective, entries, result));
+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,
@@ -80,7 +82,7 @@
   {master = "", header = Thy_Header.make ("", Position.none) [] [], errors = []};
 val no_perspective = make_perspective (false, [], []);
 
-val empty_node = make_node (no_header, NONE, no_perspective, Entries.empty, NONE);
+val empty_node = 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
@@ -88,12 +90,13 @@
   is_none visible_last andalso
   Inttab.is_empty overlays;
 
-fun is_empty_node (Node {header, keywords, perspective, entries, result}) =
+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;
+  is_none result andalso
+  Lazy.is_finished consolidated;
 
 
 (* basic components *)
@@ -104,14 +107,15 @@
   | _ => Path.current);
 
 fun set_header master header errors =
-  map_node (fn (_, keywords, perspective, entries, result) =>
-    ({master = master, header = header, errors = errors}, keywords, perspective, entries, result));
+  map_node (fn (_, keywords, perspective, entries, result, consolidated) =>
+    ({master = master, header = header, errors = errors},
+      keywords, perspective, entries, result, consolidated));
 
 fun get_header (Node {header, ...}) = header;
 
 fun set_keywords keywords =
-  map_node (fn (header, _, perspective, entries, result) =>
-    (header, keywords, perspective, entries, result));
+  map_node (fn (header, _, perspective, entries, result, consolidated) =>
+    (header, keywords, perspective, entries, result, consolidated));
 
 fun get_keywords (Node {keywords, ...}) = keywords;
 
@@ -134,8 +138,8 @@
 fun get_perspective (Node {perspective, ...}) = perspective;
 
 fun set_perspective args =
-  map_node (fn (header, keywords, _, entries, result) =>
-    (header, keywords, make_perspective args, entries, result));
+  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;
@@ -144,8 +148,8 @@
 val overlays = Inttab.lookup_list o #overlays o get_perspective;
 
 fun map_entries f =
-  map_node (fn (header, keywords, perspective, entries, result) =>
-    (header, keywords, perspective, f entries, result));
+  map_node (fn (header, keywords, perspective, entries, result, consolidated) =>
+    (header, keywords, perspective, f entries, result, consolidated));
 
 fun get_entries (Node {entries, ...}) = entries;
 
@@ -158,14 +162,8 @@
 fun get_result (Node {result, ...}) = result;
 
 fun set_result result =
-  map_node (fn (header, keywords, perspective, entries, _) =>
-    (header, keywords, perspective, entries, result));
-
-fun changed_result node node' =
-  (case (get_result node, get_result node') of
-    (SOME eval, SOME eval') => not (Command.eval_eq (eval, eval'))
-  | (NONE, NONE) => false
-  | _ => true);
+  map_node (fn (header, keywords, perspective, entries, _, consolidated) =>
+    (header, keywords, perspective, entries, result, consolidated));
 
 fun pending_result node =
   (case get_result node of
@@ -177,6 +175,35 @@
     SOME eval => Command.eval_finished eval
   | NONE => false);
 
+fun finished_result_theory node =
+  finished_result node andalso
+    let val st = Command.eval_result_state (the (get_result node))
+    in (Toplevel.end_theory Position.none st; true) handle ERROR _ => false end;
+
+val reset_consolidated =
+  map_node (fn (header, keywords, perspective, entries, result, _) =>
+    (header, keywords, perspective, entries, result, Lazy.lazy I));
+
+fun check_consolidated (node as Node {consolidated, ...}) =
+  Lazy.is_finished consolidated orelse
+  finished_result_theory node andalso
+    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
+        [] =>
+         (Lazy.force consolidated;
+          Position.setmp_thread_data (Position.id_only (Document_ID.print result_id))
+            (fn () => Output.status (Markup.markup_only Markup.consolidated)) ();
+          true)
+      | _ => false)
+    end;
+
 fun get_node nodes name = String_Graph.get_node nodes name
   handle String_Graph.UNDEF _ => empty_node;
 fun default_node name = String_Graph.default_node (name, empty_node);
@@ -400,10 +427,16 @@
 
 val the_command_name = #1 oo the_command;
 
+
+(* execution *)
+
+fun get_execution (State {execution, ...}) = execution;
+fun get_execution_version state = the_version state (#version_id (get_execution state));
+
 fun command_exec state node_name command_id =
   let
-    val State {execution = {version_id, ...}, ...} = state;
-    val node = get_node (nodes_of (the_version state version_id)) node_name;
+    val version = get_execution_version state;
+    val node = get_node (nodes_of version) node_name;
   in the_entry node command_id end;
 
 end;
@@ -492,6 +525,10 @@
         {version_id = version_id, execution_id = execution_id, delay_request = delay_request'};
     in (versions, blobs, commands, execution') end));
 
+fun consolidate_execution state =
+  String_Graph.fold (fn (_, (node, _)) => fn () => ignore (check_consolidated node))
+    (nodes_of (get_execution_version state)) ();
+
 
 
 (** document update **)
@@ -702,11 +739,13 @@
                         val removed = maps (removed_execs node0) assign_update;
                         val _ = List.app Execution.cancel removed;
 
+                        val result_changed =
+                          not (eq_option Command.eval_eq (get_result node0, result));
                         val node' = node
                           |> assign_update_apply assigned_execs
-                          |> set_result result;
+                          |> set_result result
+                          |> result_changed ? reset_consolidated;
                         val assigned_node = SOME (name, node');
-                        val result_changed = changed_result node0 node';
                       in ((removed, assign_update, assigned_node, result_changed), node') end
                     else (([], [], NONE, false), node)
                   end))))

--- a/src/Pure/PIDE/document.scala	Tue Aug 08 12:21:29 2017 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Aug 08 22:13:05 2017 +0200
@@ -453,6 +453,7 @@
 
     def node_name: Node.Name
     def node: Node
+    def node_consolidated: Boolean
 
     def commands_loading: List[Command]
     def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range]
@@ -791,6 +792,11 @@
       } yield tree).toList
     }
 
+    def node_consolidated(version: Version, name: Node.Name): Boolean =
+      !name.is_theory ||
+        version.nodes(name).commands.reverse.iterator.
+          flatMap(command_states(version, _)).exists(_.consolidated)
+
     // persistent user-view
     def snapshot(name: Node.Name = Node.Name.empty, pending_edits: List[Text.Edit] = Nil)
       : Snapshot =
@@ -835,6 +841,8 @@
         val node_name: Node.Name = name
         val node: Node = version.nodes(name)
 
+        def node_consolidated: Boolean = state.node_consolidated(version, node_name)
+
         val commands_loading: List[Command] =
           if (node_name.is_theory) Nil
           else version.nodes.commands_loading(node_name)

--- a/src/Pure/PIDE/markup.ML	Tue Aug 08 12:21:29 2017 +0200
+++ b/src/Pure/PIDE/markup.ML	Tue Aug 08 22:13:05 2017 +0200
@@ -159,6 +159,7 @@
   val runningN: string val running: T
   val finishedN: string val finished: T
   val failedN: string val failed: T
+  val consolidatedN: string val consolidated: T
   val exec_idN: string
   val initN: string
   val statusN: string val status: T
@@ -555,6 +556,7 @@
 val (runningN, running) = markup_elem "running";
 val (finishedN, finished) = markup_elem "finished";
 val (failedN, failed) = markup_elem "failed";
+val (consolidatedN, consolidated) = markup_elem "consolidated";
 
 
 (* messages *)

--- a/src/Pure/PIDE/markup.scala	Tue Aug 08 12:21:29 2017 +0200
+++ b/src/Pure/PIDE/markup.scala	Tue Aug 08 22:13:05 2017 +0200
@@ -423,6 +423,7 @@
   val RUNNING = "running"
   val FINISHED = "finished"
   val FAILED = "failed"
+  val CONSOLIDATED = "consolidated"
 
 
   /* interactive documents */

--- a/src/Pure/PIDE/protocol.ML	Tue Aug 08 12:21:29 2017 +0200
+++ b/src/Pure/PIDE/protocol.ML	Tue Aug 08 22:13:05 2017 +0200
@@ -58,6 +58,10 @@
       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 ());
 

--- a/src/Pure/PIDE/protocol.scala	Tue Aug 08 12:21:29 2017 +0200
+++ b/src/Pure/PIDE/protocol.scala	Tue Aug 08 22:13:05 2017 +0200
@@ -352,6 +352,9 @@
 
   /* execution */
 
+  def consolidate_execution(): Unit =
+    protocol_command("Document.consolidate_execution")
+
   def discontinue_execution(): Unit =
     protocol_command("Document.discontinue_execution")
 

--- a/src/Pure/PIDE/session.scala	Tue Aug 08 12:21:29 2017 +0200
+++ b/src/Pure/PIDE/session.scala	Tue Aug 08 22:13:05 2017 +0200
@@ -130,6 +130,7 @@
   /* dynamic session options */
 
   def output_delay: Time = session_options.seconds("editor_output_delay")
+  def consolidate_delay: Time = session_options.seconds("editor_consolidate_delay")
   def prune_delay: Time = session_options.seconds("editor_prune_delay")
   def prune_size: Int = session_options.int("editor_prune_size")
   def syslog_limit: Int = session_options.int("editor_syslog_limit")
@@ -191,6 +192,7 @@
   private case class Cancel_Exec(exec_id: Document_ID.Exec)
   private case class Protocol_Command(name: String, args: List[String])
   private case class Update_Options(options: Options)
+  private case object Consolidate_Execution
   private case object Prune_History
 
 
@@ -519,6 +521,9 @@
               prover.get.terminate
             }
 
+          case Consolidate_Execution =>
+            if (prover.defined) prover.get.consolidate_execution()
+
           case Prune_History =>
             if (prover.defined) {
               val old_versions = global_state.change_result(_.remove_versions(prune_size))
@@ -564,6 +569,28 @@
     }
   }
 
+  private val consolidator: Thread =
+    Standard_Thread.fork("Session.consolidator", daemon = true) {
+      try {
+        while (true) {
+          Thread.sleep(consolidate_delay.ms)
+
+          val state = global_state.value
+          state.stable_tip_version match {
+            case None =>
+            case Some(version) =>
+              val consolidated =
+                version.nodes.iterator.forall(
+                  { case (name, _) =>
+                      resources.session_base.loaded_theory(name) ||
+                      state.node_consolidated(version, name) })
+              if (!consolidated) manager.send(Consolidate_Execution)
+          }
+        }
+      }
+      catch { case Exn.Interrupt() => }
+    }
+
 
   /* main operations */
 
@@ -602,6 +629,8 @@
 
     change_parser.shutdown()
     change_buffer.shutdown()
+    consolidator.interrupt
+    consolidator.join
     manager.shutdown()
     dispatcher.shutdown()