--- a/src/Pure/PIDE/document_status.scala Mon Sep 03 18:52:28 2018 +0200
+++ b/src/Pure/PIDE/document_status.scala Mon Sep 03 19:44:10 2018 +0200
@@ -164,10 +164,16 @@
def quasi_consolidated: Boolean = !finalized && terminated
+ def percentage: Int =
+ if (consolidated) 100
+ else if (total == 0) 0
+ else (((total - unprocessed).toDouble / total) * 100).toInt min 99
+
def json: JSON.Object.T =
JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
"running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished,
- "canceled" -> canceled, "consolidated" -> consolidated)
+ "canceled" -> canceled, "consolidated" -> consolidated,
+ "percentage" -> percentage)
}