src/Pure/PIDE/command.scala

--- a/src/Pure/PIDE/command.scala	Fri Aug 17 21:34:56 2018 +0200
+++ b/src/Pure/PIDE/command.scala	Sat Aug 18 12:41:05 2018 +0200
@@ -263,9 +263,24 @@
     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 maybe_consolidated: Boolean =
+    {
+      var touched = false
+      var forks = 0
+      var runs = 0
+      for (markup <- status) {
+        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
+    }
 
-    lazy val protocol_status: Protocol.Status =
+    lazy val document_status: Document_Status.Command_Status =
     {
       val warnings =
         if (results.iterator.exists(p => Protocol.is_warning(p._2) || Protocol.is_legacy(p._2)))
@@ -275,7 +290,7 @@
         if (results.iterator.exists(p => Protocol.is_error(p._2)))
           List(Markup(Markup.ERROR, Nil))
         else Nil
-      Protocol.Status.make((warnings ::: errors ::: status).iterator)
+      Document_Status.Command_Status.make((warnings ::: errors ::: status).iterator)
     }
 
     def markup(index: Markup_Index): Markup_Tree = markups(index)
@@ -301,7 +316,7 @@
       status: Boolean, chunk_name: Symbol.Text_Chunk.Name, m: Text.Markup): State =
     {
       val markups1 =
-        if (status || Protocol.liberal_status_elements(m.info.name))
+        if (status || Document_Status.Command_Status.liberal_elements(m.info.name))
           markups.add(Markup_Index(true, chunk_name), m)
         else markups
       copy(markups = markups1.add(Markup_Index(false, chunk_name), m))