diff -r f249e1f5623b -r 2fd3a6d6ba2e src/Pure/PIDE/session.scala
--- 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()