src/Pure/PIDE/document_status.scala
changeset 83266 2f75f2495e3e
parent 83247 fbba662ca976
child 83289 2cd87a6da20b
--- a/src/Pure/PIDE/document_status.scala	Sat Oct 11 16:19:16 2025 +0200
+++ b/src/Pure/PIDE/document_status.scala	Sun Oct 12 15:11:29 2025 +0200
@@ -326,6 +326,9 @@
 
     def quasi_consolidated: Boolean = !suppressed && !finalized && terminated
 
+    def started: Boolean = percentage == 0
+    def completed: Boolean = percentage == 100
+
     def json: JSON.Object.T =
       JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
         "running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished,