more node status information;
authorwenzelm
Tue May 29 22:25:59 2018 +0200 (12 months ago)
changeset 68323bf7336731981
parent 68322 100f018096c8
child 68324 88c07fabd5b4
more node status information;
src/Doc/System/Server.thy
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.ML
src/Pure/PIDE/document.scala
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/PIDE/protocol.scala
     1.1 --- a/src/Doc/System/Server.thy	Tue May 29 20:03:24 2018 +0200
     1.2 +++ b/src/Doc/System/Server.thy	Tue May 29 22:25:59 2018 +0200
     1.3 @@ -516,13 +516,14 @@
     1.4    session-qualified theory name (e.g.\ \<^verbatim>\<open>HOL-ex.Seq\<close>).
     1.5  
     1.6    \<^item> \<^bold>\<open>type\<close> \<open>node_status = {ok: bool, total: int, unprocessed: int, running:
     1.7 -  int, warned: int, failed: int, finished: int, consolidated: bool}\<close>
     1.8 -  represents a formal theory node status of the PIDE document model. Fields
     1.9 -  \<open>total\<close>, \<open>unprocessed\<close>, \<open>running\<close>, \<open>warned\<close>, \<open>failed\<close>, \<open>finished\<close> account
    1.10 -  for individual commands within a theory node; \<open>ok\<close> is an abstraction for
    1.11 -  \<open>failed = 0\<close>. The \<open>consolidated\<close> flag indicates whether the outermost theory
    1.12 -  command structure has finished (or failed) and the final \<^theory_text>\<open>end\<close> command has
    1.13 -  been checked.
    1.14 +  int, warned: int, failed: int, finished: int, initialized: bool,
    1.15 +  consolidated: bool}\<close> represents a formal theory node status of the PIDE
    1.16 +  document model. Fields \<open>total\<close>, \<open>unprocessed\<close>, \<open>running\<close>, \<open>warned\<close>,
    1.17 +  \<open>failed\<close>, \<open>finished\<close> account for individual commands within a theory node;
    1.18 +  \<open>ok\<close> is an abstraction for \<open>failed = 0\<close>. The \<open>initialized\<close> flag indicates
    1.19 +  that the initial \<^theory_text>\<open>theory\<close> command has been processed. The \<open>consolidated\<close>
    1.20 +  flag indicates whether the outermost theory command structure has finished
    1.21 +  (or failed) and the final \<^theory_text>\<open>end\<close> command has been checked.
    1.22  \<close>
    1.23  
    1.24  
     2.1 --- a/src/Pure/PIDE/command.scala	Tue May 29 20:03:24 2018 +0200
     2.2 +++ b/src/Pure/PIDE/command.scala	Tue May 29 22:25:59 2018 +0200
     2.3 @@ -260,6 +260,8 @@
     2.4      exports: Exports = Exports.empty,
     2.5      markups: Markups = Markups.empty)
     2.6    {
     2.7 +    def initialized: Boolean = status.exists(markup => markup.name == Markup.INITIALIZED)
     2.8 +
     2.9      lazy val consolidated: Boolean =
    2.10        status.exists(markup => markup.name == Markup.CONSOLIDATED)
    2.11  
    2.12 @@ -565,6 +567,8 @@
    2.13    val is_unparsed: Boolean = span.content.exists(_.is_unparsed)
    2.14    val is_unfinished: Boolean = span.content.exists(_.is_unfinished)
    2.15  
    2.16 +  def potentially_initialized: Boolean = span.name == Thy_Header.THEORY
    2.17 +
    2.18  
    2.19    /* blobs */
    2.20  
     3.1 --- a/src/Pure/PIDE/document.ML	Tue May 29 20:03:24 2018 +0200
     3.2 +++ b/src/Pure/PIDE/document.ML	Tue May 29 22:25:59 2018 +0200
     3.3 @@ -633,7 +633,9 @@
     3.4      val parents =
     3.5        if null parents_reports then [Theory.get_pure ()] else map #1 parents_reports;
     3.6      val _ = Position.reports (map #2 parents_reports);
     3.7 -  in Resources.begin_theory master_dir header parents end;
     3.8 +    val thy = Resources.begin_theory master_dir header parents;
     3.9 +    val _ = Output.status (Markup.markup_only Markup.initialized);
    3.10 +  in thy end;
    3.11  
    3.12  fun check_root_theory node =
    3.13    let
     4.1 --- a/src/Pure/PIDE/document.scala	Tue May 29 20:03:24 2018 +0200
     4.2 +++ b/src/Pure/PIDE/document.scala	Tue May 29 22:25:59 2018 +0200
     4.3 @@ -921,6 +921,13 @@
     4.4        }
     4.5      }
     4.6  
     4.7 +    def node_initialized(version: Version, name: Node.Name): Boolean =
     4.8 +      name.is_theory &&
     4.9 +      (version.nodes(name).commands.iterator.find(_.potentially_initialized) match {
    4.10 +        case None => false
    4.11 +        case Some(command) => command_states(version, command).headOption.exists(_.initialized)
    4.12 +      })
    4.13 +
    4.14      def node_consolidated(version: Version, name: Node.Name): Boolean =
    4.15        !name.is_theory ||
    4.16          version.nodes(name).commands.reverse.iterator.
     5.1 --- a/src/Pure/PIDE/markup.ML	Tue May 29 20:03:24 2018 +0200
     5.2 +++ b/src/Pure/PIDE/markup.ML	Tue May 29 22:25:59 2018 +0200
     5.3 @@ -167,6 +167,7 @@
     5.4    val runningN: string val running: T
     5.5    val finishedN: string val finished: T
     5.6    val failedN: string val failed: T
     5.7 +  val initializedN: string val initialized: T
     5.8    val consolidatedN: string val consolidated: T
     5.9    val exec_idN: string
    5.10    val initN: string
    5.11 @@ -580,6 +581,8 @@
    5.12  val (runningN, running) = markup_elem "running";
    5.13  val (finishedN, finished) = markup_elem "finished";
    5.14  val (failedN, failed) = markup_elem "failed";
    5.15 +
    5.16 +val (initializedN, initialized) = markup_elem "initialized";
    5.17  val (consolidatedN, consolidated) = markup_elem "consolidated";
    5.18  
    5.19  
     6.1 --- a/src/Pure/PIDE/markup.scala	Tue May 29 20:03:24 2018 +0200
     6.2 +++ b/src/Pure/PIDE/markup.scala	Tue May 29 22:25:59 2018 +0200
     6.3 @@ -426,6 +426,8 @@
     6.4    val RUNNING = "running"
     6.5    val FINISHED = "finished"
     6.6    val FAILED = "failed"
     6.7 +
     6.8 +  val INITIALIZED = "initialized"
     6.9    val CONSOLIDATED = "consolidated"
    6.10  
    6.11  
     7.1 --- a/src/Pure/PIDE/protocol.scala	Tue May 29 20:03:24 2018 +0200
     7.2 +++ b/src/Pure/PIDE/protocol.scala	Tue May 29 22:25:59 2018 +0200
     7.3 @@ -142,7 +142,8 @@
     7.4    /* node status */
     7.5  
     7.6    sealed case class Node_Status(
     7.7 -    unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int, consolidated: Boolean)
     7.8 +    unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int,
     7.9 +    initialized: Boolean, consolidated: Boolean)
    7.10    {
    7.11      def ok: Boolean = failed == 0
    7.12      def total: Int = unprocessed + running + warned + failed + finished
    7.13 @@ -150,7 +151,7 @@
    7.14      def json: JSON.Object.T =
    7.15        JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
    7.16          "running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished,
    7.17 -        "consolidated" -> consolidated)
    7.18 +        "initialized" -> initialized, "consolidated" -> consolidated)
    7.19    }
    7.20  
    7.21    def node_status(
    7.22 @@ -175,9 +176,10 @@
    7.23        else if (status.is_finished) finished += 1
    7.24        else unprocessed += 1
    7.25      }
    7.26 +    val initialized = state.node_initialized(version, name)
    7.27      val consolidated = state.node_consolidated(version, name)
    7.28  
    7.29 -    Node_Status(unprocessed, running, warned, failed, finished, consolidated)
    7.30 +    Node_Status(unprocessed, running, warned, failed, finished, initialized, consolidated)
    7.31    }
    7.32  
    7.33