src/Pure/PIDE/document_status.scala
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