diff -r b11587195c70 -r 2f75f2495e3e src/Pure/PIDE/document_status.scala --- 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,