less wasteful consolidation, based on PIDE front-end state and recent changes;

--- a/etc/options	Tue Jun 05 14:15:49 2018 +0200
+++ b/etc/options	Tue Jun 05 16:12:26 2018 +0200
@@ -156,7 +156,7 @@
 public option editor_output_delay : real = 0.1
   -- "delay for prover output (markup, common messages etc.)"
 
-public option editor_consolidate_delay : real = 2.5
+public option editor_consolidate_delay : real = 2.0
   -- "delay to consolidate status of command evaluation (execution forks)"
 
 public option editor_prune_delay : real = 15

--- a/src/Pure/PIDE/command.scala	Tue Jun 05 14:15:49 2018 +0200
+++ b/src/Pure/PIDE/command.scala	Tue Jun 05 16:12:26 2018 +0200
@@ -263,6 +263,8 @@
     def initialized: Boolean = status.exists(markup => markup.name == Markup.INITIALIZED)
     def consolidated: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATED)
 
+    lazy val maybe_consolidated: Boolean = Protocol.maybe_consolidated(status)
+
     lazy val protocol_status: Protocol.Status =
     {
       val warnings =

--- a/src/Pure/PIDE/document.ML	Tue Jun 05 14:15:49 2018 +0200
+++ b/src/Pure/PIDE/document.ML	Tue Jun 05 16:12:26 2018 +0200
@@ -24,7 +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 update: Document_ID.version -> Document_ID.version -> edit list -> bool -> state ->
+  val update: Document_ID.version -> Document_ID.version -> edit list -> string list -> state ->
     Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state
   val state: unit -> state
   val change_state: (state -> state) -> unit
@@ -768,6 +768,7 @@
       timeit "Document.edit_nodes"
         (fn () => old_version |> fold edit_nodes edits |> edit_keywords edits);
 
+    val consolidate = Symtab.defined (Symtab.make_set consolidate);
     val nodes = nodes_of new_version;
     val required = make_required nodes;
     val required0 = make_required (nodes_of old_version);
@@ -786,7 +787,7 @@
                     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 maybe_consolidate = consolidate name 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;

--- a/src/Pure/PIDE/document.scala	Tue Jun 05 14:15:49 2018 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Jun 05 16:12:26 2018 +0200
@@ -849,6 +849,18 @@
         removing_versions = false)
     }
 
+    def command_state_eval(version: Version, command: Command): Option[Command.State] =
+    {
+      require(is_assigned(version))
+      try {
+        the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil) match {
+          case eval_id :: _ => Some(the_dynamic_state(eval_id))
+          case Nil => None
+        }
+      }
+      catch { case _: State.Fail => None }
+    }
+
     private def command_states_self(version: Version, command: Command)
       : List[(Document_ID.Generic, Command.State)] =
     {
@@ -930,6 +942,16 @@
         case Some(command) => command_states(version, command).headOption.exists(_.initialized)
       })
 
+    def node_maybe_consolidated(version: Version, name: Node.Name): Boolean =
+      name.is_theory &&
+      {
+        version.nodes(name).commands.reverse.iterator.forall(command =>
+          command_state_eval(version, command) match {
+            case None => false
+            case Some(st) => st.maybe_consolidated
+          })
+      }
+
     def node_consolidated(version: Version, name: Node.Name): Boolean =
       !name.is_theory ||
       {

--- a/src/Pure/PIDE/protocol.ML	Tue Jun 05 14:15:49 2018 +0200
+++ b/src/Pure/PIDE/protocol.ML	Tue Jun 05 16:12:26 2018 +0200
@@ -74,7 +74,7 @@
 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, consolidate_string] =>
+      (fn [old_id_string, new_id_string, edits_yxml, consolidate_yxml] =>
         Document.change_state (fn state =>
           let
             val old_id = Document_ID.parse old_id_string;
@@ -100,7 +100,9 @@
                         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 consolidate =
+              YXML.parse_body consolidate_yxml |>
+                let open XML.Decode in list string end;
 
             val _ = Execution.discontinue ();
 

--- a/src/Pure/PIDE/protocol.scala	Tue Jun 05 14:15:49 2018 +0200
+++ b/src/Pure/PIDE/protocol.scala	Tue Jun 05 16:12:26 2018 +0200
@@ -38,6 +38,26 @@
   }
 
 
+  /* consolidation status */
+
+  def maybe_consolidated(markups: List[Markup]): Boolean =
+  {
+    var touched = false
+    var forks = 0
+    var runs = 0
+    for (markup <- markups) {
+      markup.name match {
+        case Markup.FORKED => touched = true; forks += 1
+        case Markup.JOINED => forks -= 1
+        case Markup.RUNNING => touched = true; runs += 1
+        case Markup.FINISHED => runs -= 1
+        case _ =>
+      }
+    }
+    touched && forks == 0 && runs == 0
+  }
+
+
   /* command status */
 
   object Status
@@ -419,7 +439,7 @@
   /* document versions */
 
   def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
-    edits: List[Document.Edit_Command], consolidate: Boolean)
+    edits: List[Document.Edit_Command], consolidate: List[Document.Node.Name])
   {
     val edits_yxml =
     {
@@ -446,9 +466,17 @@
         val (name, edit) = node_edit
         pair(string, encode_edit(name))(name.node, edit)
       })
-      Symbol.encode_yxml(encode_edits(edits)) }
+      Symbol.encode_yxml(encode_edits(edits))
+    }
+
+    val consolidate_yxml =
+    {
+      import XML.Encode._
+      Symbol.encode_yxml(list(string)(consolidate.map(_.node)))
+    }
+
     protocol_command(
-      "Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml, consolidate.toString)
+      "Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml, consolidate_yxml)
   }
 
   def remove_versions(versions: List[Document.Version])

--- a/src/Pure/PIDE/resources.scala	Tue Jun 05 14:15:49 2018 +0200
+++ b/src/Pure/PIDE/resources.scala	Tue Jun 05 16:12:26 2018 +0200
@@ -216,7 +216,7 @@
       previous: Document.Version,
       doc_blobs: Document.Blobs,
       edits: List[Document.Edit_Text],
-      consolidate: Boolean): Session.Change =
+      consolidate: List[Document.Node.Name]): Session.Change =
     Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits, consolidate)
 
   def commit(change: Session.Change) { }

--- a/src/Pure/PIDE/session.scala	Tue Jun 05 14:15:49 2018 +0200
+++ b/src/Pure/PIDE/session.scala	Tue Jun 05 16:12:26 2018 +0200
@@ -50,7 +50,7 @@
     syntax_changed: List[Document.Node.Name],
     deps_changed: Boolean,
     doc_edits: List[Document.Edit_Command],
-    consolidate: Boolean,
+    consolidate: List[Document.Node.Name],
     version: Document.Version)
 
   case object Change_Flush
@@ -231,7 +231,7 @@
     previous: Future[Document.Version],
     doc_blobs: Document.Blobs,
     text_edits: List[Document.Edit_Text],
-    consolidate: Boolean,
+    consolidate: List[Document.Node.Name],
     version_result: Promise[Document.Version])
 
   private val change_parser = Consumer_Thread.fork[Text_Edits]("change_parser", daemon = true)
@@ -259,6 +259,7 @@
     def flush(): Unit = synchronized {
       if (assignment || nodes.nonEmpty || commands.nonEmpty)
         commands_changed.post(Session.Commands_Changed(assignment, nodes, commands))
+      if (nodes.nonEmpty) consolidation.update(nodes)
       assignment = false
       nodes = Set.empty
       commands = Set.empty
@@ -299,6 +300,28 @@
   }
 
 
+  /* node consolidation */
+
+  private object consolidation
+  {
+    private val delay =
+      Standard_Thread.delay_first(consolidate_delay) { manager.send(Consolidate_Execution) }
+
+    private val changed_nodes = Synchronized(Set.empty[Document.Node.Name])
+
+    def update(new_nodes: Set[Document.Node.Name] = Set.empty)
+    {
+      changed_nodes.change(nodes => if (nodes.isEmpty) new_nodes else nodes ++ new_nodes)
+      delay.invoke()
+    }
+
+    def flush(): Set[Document.Node.Name] =
+      changed_nodes.change_result(nodes => (nodes, Set.empty))
+
+    def shutdown() { delay.revoke() }
+  }
+
+
   /* prover process */
 
   private object prover
@@ -347,7 +370,7 @@
     def handle_raw_edits(
       doc_blobs: Document.Blobs = Document.Blobs.empty,
       edits: List[Document.Edit_Text] = Nil,
-      consolidate: Boolean = false)
+      consolidate: List[Document.Node.Name] = Nil)
     //{{{
     {
       require(prover.defined)
@@ -534,7 +557,19 @@
             }
 
           case Consolidate_Execution =>
-            if (prover.defined) handle_raw_edits(consolidate = true)
+            if (prover.defined) {
+              val state = global_state.value
+              state.stable_tip_version match {
+                case None => consolidation.update()
+                case Some(version) =>
+                  val consolidate =
+                    consolidation.flush().iterator.filter(name =>
+                      !resources.session_base.loaded_theory(name) &&
+                      !state.node_consolidated(version, name) &&
+                      state.node_maybe_consolidated(version, name)).toList
+                  if (consolidate.nonEmpty) handle_raw_edits(consolidate = consolidate)
+              }
+            }
 
           case Prune_History =>
             if (prover.defined) {
@@ -581,28 +616,6 @@
     }
   }
 
-  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 */
 
@@ -641,8 +654,7 @@
 
     change_parser.shutdown()
     change_buffer.shutdown()
-    consolidator.interrupt
-    consolidator.join
+    consolidation.shutdown()
     manager.shutdown()
     dispatcher.shutdown()
 

--- a/src/Pure/Thy/thy_syntax.scala	Tue Jun 05 14:15:49 2018 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Tue Jun 05 16:12:26 2018 +0200
@@ -297,7 +297,7 @@
       previous: Document.Version,
       doc_blobs: Document.Blobs,
       edits: List[Document.Edit_Text],
-      consolidate: Boolean): Session.Change =
+      consolidate: List[Document.Node.Name]): Session.Change =
   {
     val (syntax_changed, nodes0, doc_edits0) = header_edits(resources, previous, edits)