diff -r e7e3776385ba -r a110e7e24e55 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Fri Aug 17 21:34:56 2018 +0200
+++ b/src/Pure/PIDE/protocol.scala	Sat Aug 18 12:41:05 2018 +0200
@@ -38,95 +38,6 @@
   }
 
 
-  /* 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
-  {
-    def make(markup_iterator: Iterator[Markup]): Status =
-    {
-      var touched = false
-      var accepted = false
-      var warned = false
-      var failed = false
-      var forks = 0
-      var runs = 0
-      for (markup <- markup_iterator) {
-        markup.name match {
-          case Markup.ACCEPTED => accepted = true
-          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 Markup.WARNING | Markup.LEGACY => warned = true
-          case Markup.FAILED | Markup.ERROR => failed = true
-          case _ =>
-        }
-      }
-      Status(touched, accepted, warned, failed, forks, runs)
-    }
-
-    val empty = make(Iterator.empty)
-
-    def merge(status_iterator: Iterator[Status]): Status =
-      if (status_iterator.hasNext) {
-        val status0 = status_iterator.next
-        (status0 /: status_iterator)(_ + _)
-      }
-      else empty
-  }
-
-  sealed case class Status(
-    private val touched: Boolean,
-    private val accepted: Boolean,
-    private val warned: Boolean,
-    private val failed: Boolean,
-    forks: Int,
-    runs: Int)
-  {
-    def + (that: Status): Status =
-      Status(
-        touched || that.touched,
-        accepted || that.accepted,
-        warned || that.warned,
-        failed || that.failed,
-        forks + that.forks,
-        runs + that.runs)
-
-    def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0))
-    def is_running: Boolean = runs != 0
-    def is_warned: Boolean = warned
-    def is_failed: Boolean = failed
-    def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0
-  }
-
-  val proper_status_elements =
-    Markup.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
-      Markup.FINISHED, Markup.FAILED)
-
-  val liberal_status_elements =
-    proper_status_elements + Markup.WARNING + Markup.LEGACY + Markup.ERROR
-
-
   /* command timing */
 
   object Command_Timing
@@ -159,80 +70,6 @@
   }
 
 
-  /* node status */
-
-  sealed case class Node_Status(
-    unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int,
-    initialized: Boolean, consolidated: Boolean)
-  {
-    def ok: Boolean = failed == 0
-    def total: Int = unprocessed + running + warned + failed + finished
-
-    def json: JSON.Object.T =
-      JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
-        "running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished,
-        "initialized" -> initialized, "consolidated" -> consolidated)
-  }
-
-  def node_status(
-    state: Document.State,
-    version: Document.Version,
-    name: Document.Node.Name): Node_Status =
-  {
-    val node = version.nodes(name)
-
-    var unprocessed = 0
-    var running = 0
-    var warned = 0
-    var failed = 0
-    var finished = 0
-    for (command <- node.commands.iterator) {
-      val states = state.command_states(version, command)
-      val status = Status.merge(states.iterator.map(_.protocol_status))
-
-      if (status.is_running) running += 1
-      else if (status.is_failed) failed += 1
-      else if (status.is_warned) warned += 1
-      else if (status.is_finished) finished += 1
-      else unprocessed += 1
-    }
-    val initialized = state.node_initialized(version, name)
-    val consolidated = state.node_consolidated(version, name)
-
-    Node_Status(unprocessed, running, warned, failed, finished, initialized, consolidated)
-  }
-
-
-  /* node timing */
-
-  sealed case class Node_Timing(total: Double, commands: Map[Command, Double])
-
-  val empty_node_timing = Node_Timing(0.0, Map.empty)
-
-  def node_timing(
-    state: Document.State,
-    version: Document.Version,
-    node: Document.Node,
-    threshold: Double): Node_Timing =
-  {
-    var total = 0.0
-    var commands = Map.empty[Command, Double]
-    for {
-      command <- node.commands.iterator
-      st <- state.command_states(version, command)
-    } {
-      val command_timing =
-        (0.0 /: st.status)({
-          case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds
-          case (timing, _) => timing
-        })
-      total += command_timing
-      if (command_timing >= threshold) commands += (command -> command_timing)
-    }
-    Node_Timing(total, commands)
-  }
-
-
   /* result messages */
 
   def is_result(msg: XML.Tree): Boolean =