--- a/src/Doc/System/Server.thy Mon Sep 03 18:52:28 2018 +0200
+++ b/src/Doc/System/Server.thy Mon Sep 03 19:44:10 2018 +0200
@@ -517,8 +517,8 @@
\<^item> \<^bold>\<open>type\<close> \<open>node_status = {ok: bool, total: int, unprocessed: int, running:
int, warned: int, failed: int, finished: int, canceled: bool, consolidated:
- bool}\<close> represents a formal theory node status of the PIDE document model as
- follows.
+ bool, percentage: int}\<close> represents a formal theory node status of the PIDE
+ document model as follows.
\<^item> Fields \<open>total\<close>, \<open>unprocessed\<close>, \<open>running\<close>, \<open>warned\<close>, \<open>failed\<close>, \<open>finished\<close>
account for individual commands within a theory node; \<open>ok\<close> is an
@@ -531,9 +531,14 @@
\<^item> The \<open>consolidated\<close> flag indicates whether the outermost theory command
structure has finished (or failed) and the final \<^theory_text>\<open>end\<close> command has been
checked.
+
+ \<^item> The \<open>percentage\<close> field tells how far the node has been processed. It
+ ranges between 0 and 99 in normal operation, and reaches 100 when the node
+ has been formally consolidated as described above.
\<close>
+
section \<open>Server commands and results\<close>
text \<open>
--- 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)
}