--- a/src/Pure/PIDE/document_status.scala Mon Sep 03 18:47:31 2018 +0200
+++ b/src/Pure/PIDE/document_status.scala Mon Sep 03 18:52:28 2018 +0200
@@ -162,6 +162,8 @@
def ok: Boolean = failed == 0
def total: Int = unprocessed + running + warned + failed + finished
+ def quasi_consolidated: Boolean = !finalized && terminated
+
def json: JSON.Object.T =
JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
"running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished,
@@ -225,7 +227,7 @@
def quasi_consolidated(name: Document.Node.Name): Boolean =
rep.get(name) match {
- case Some(st) => !st.finalized && st.terminated
+ case Some(st) => st.quasi_consolidated
case None => false
}