| changeset 83298 | d2ffec6f4b89 |
| parent 83297 | 00bb83e60336 |
| child 83503 | 7b1b7ac616c0 |
--- a/src/Pure/PIDE/document_status.scala Fri Oct 17 15:13:45 2025 +0200 +++ b/src/Pure/PIDE/document_status.scala Fri Oct 17 15:19:01 2025 +0200 @@ -341,6 +341,8 @@ def quasi_consolidated: Boolean = !suppressed && !finalized && terminated + def progress: Boolean = running > 0 || command_timings.valuesIterator.exists(_.has_running) + def started: Boolean = percentage == 0 def completed: Boolean = percentage == 100