# HG changeset patch
# User wenzelm
# Date 1535993548 -7200
# Node ID bdc38f0fd68c8b62491bb4b008ffdf312d61b4f7
# Parent  e63eaae131655e9488205eed32799eab3339b682
tuned signature;

diff -r e63eaae13165 -r bdc38f0fd68c src/Pure/PIDE/document_status.scala
--- 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
       }