# HG changeset patch
# User wenzelm
# Date 1535996650 -7200
# Node ID 241d08beaf5c4f6b5527347047f047c477f39524
# Parent  bdc38f0fd68c8b62491bb4b008ffdf312d61b4f7
more informative node_status;

diff -r bdc38f0fd68c -r 241d08beaf5c src/Doc/System/Server.thy
--- 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>
diff -r bdc38f0fd68c -r 241d08beaf5c src/Pure/PIDE/document_status.scala
--- 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)
   }