changeset 69844 | b21ddfa7042b |
parent 69818 | 60d0ee8f2ddb |
child 69863 | 9532d5b2e932 |
--- a/src/Pure/PIDE/document_status.scala Wed Feb 27 14:22:00 2019 +0100 +++ b/src/Pure/PIDE/document_status.scala Wed Feb 27 16:28:46 2019 +0100 @@ -164,7 +164,7 @@ def ok: Boolean = failed == 0 def total: Int = unprocessed + running + warned + failed + finished - def quasi_consolidated: Boolean = !finalized && terminated + def quasi_consolidated: Boolean = !is_suppressed && !finalized && terminated def percentage: Int = if (consolidated) 100