more informative node_status;
authorwenzelm
Mon Sep 03 19:44:10 2018 +0200 (9 months ago)
changeset 68898241d08beaf5c
parent 68897 bdc38f0fd68c
child 68899 b15b03c13dbb
more informative node_status;
src/Doc/System/Server.thy
src/Pure/PIDE/document_status.scala
     1.1 --- a/src/Doc/System/Server.thy	Mon Sep 03 18:52:28 2018 +0200
     1.2 +++ b/src/Doc/System/Server.thy	Mon Sep 03 19:44:10 2018 +0200
     1.3 @@ -517,8 +517,8 @@
     1.4  
     1.5    \<^item> \<^bold>\<open>type\<close> \<open>node_status = {ok: bool, total: int, unprocessed: int, running:
     1.6    int, warned: int, failed: int, finished: int, canceled: bool, consolidated:
     1.7 -  bool}\<close> represents a formal theory node status of the PIDE document model as
     1.8 -  follows.
     1.9 +  bool, percentage: int}\<close> represents a formal theory node status of the PIDE
    1.10 +  document model as follows.
    1.11  
    1.12      \<^item> Fields \<open>total\<close>, \<open>unprocessed\<close>, \<open>running\<close>, \<open>warned\<close>, \<open>failed\<close>, \<open>finished\<close>
    1.13        account for individual commands within a theory node; \<open>ok\<close> is an
    1.14 @@ -531,9 +531,14 @@
    1.15      \<^item> The \<open>consolidated\<close> flag indicates whether the outermost theory command
    1.16      structure has finished (or failed) and the final \<^theory_text>\<open>end\<close> command has been
    1.17      checked.
    1.18 +
    1.19 +    \<^item> The \<open>percentage\<close> field tells how far the node has been processed. It
    1.20 +    ranges between 0 and 99 in normal operation, and reaches 100 when the node
    1.21 +    has been formally consolidated as described above.
    1.22  \<close>
    1.23  
    1.24  
    1.25 +
    1.26  section \<open>Server commands and results\<close>
    1.27  
    1.28  text \<open>
     2.1 --- a/src/Pure/PIDE/document_status.scala	Mon Sep 03 18:52:28 2018 +0200
     2.2 +++ b/src/Pure/PIDE/document_status.scala	Mon Sep 03 19:44:10 2018 +0200
     2.3 @@ -164,10 +164,16 @@
     2.4  
     2.5      def quasi_consolidated: Boolean = !finalized && terminated
     2.6  
     2.7 +    def percentage: Int =
     2.8 +      if (consolidated) 100
     2.9 +      else if (total == 0) 0
    2.10 +      else (((total - unprocessed).toDouble / total) * 100).toInt min 99
    2.11 +
    2.12      def json: JSON.Object.T =
    2.13        JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
    2.14          "running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished,
    2.15 -        "canceled" -> canceled, "consolidated" -> consolidated)
    2.16 +        "canceled" -> canceled, "consolidated" -> consolidated,
    2.17 +        "percentage" -> percentage)
    2.18    }
    2.19  
    2.20