more node status information;

--- a/src/Doc/System/Server.thy	Tue May 29 20:03:24 2018 +0200
+++ b/src/Doc/System/Server.thy	Tue May 29 22:25:59 2018 +0200
@@ -516,13 +516,14 @@
   session-qualified theory name (e.g.\ \<^verbatim>\<open>HOL-ex.Seq\<close>).
 
   \<^item> \<^bold>\<open>type\<close> \<open>node_status = {ok: bool, total: int, unprocessed: int, running:
-  int, warned: int, failed: int, finished: int, consolidated: bool}\<close>
-  represents a formal theory node status of the PIDE document model. 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 abstraction for
-  \<open>failed = 0\<close>. 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.
+  int, warned: int, failed: int, finished: int, initialized: bool,
+  consolidated: bool}\<close> represents a formal theory node status of the PIDE
+  document model. 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 abstraction for \<open>failed = 0\<close>. The \<open>initialized\<close> flag indicates
+  that the initial \<^theory_text>\<open>theory\<close> command has been processed. 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.
 \<close>
 
 

--- a/src/Pure/PIDE/command.scala	Tue May 29 20:03:24 2018 +0200
+++ b/src/Pure/PIDE/command.scala	Tue May 29 22:25:59 2018 +0200
@@ -260,6 +260,8 @@
     exports: Exports = Exports.empty,
     markups: Markups = Markups.empty)
   {
+    def initialized: Boolean = status.exists(markup => markup.name == Markup.INITIALIZED)
+
     lazy val consolidated: Boolean =
       status.exists(markup => markup.name == Markup.CONSOLIDATED)
 
@@ -565,6 +567,8 @@
   val is_unparsed: Boolean = span.content.exists(_.is_unparsed)
   val is_unfinished: Boolean = span.content.exists(_.is_unfinished)
 
+  def potentially_initialized: Boolean = span.name == Thy_Header.THEORY
+
 
   /* blobs */
 

--- a/src/Pure/PIDE/document.ML	Tue May 29 20:03:24 2018 +0200
+++ b/src/Pure/PIDE/document.ML	Tue May 29 22:25:59 2018 +0200
@@ -633,7 +633,9 @@
     val parents =
       if null parents_reports then [Theory.get_pure ()] else map #1 parents_reports;
     val _ = Position.reports (map #2 parents_reports);
-  in Resources.begin_theory master_dir header parents end;
+    val thy = Resources.begin_theory master_dir header parents;
+    val _ = Output.status (Markup.markup_only Markup.initialized);
+  in thy end;
 
 fun check_root_theory node =
   let

--- a/src/Pure/PIDE/document.scala	Tue May 29 20:03:24 2018 +0200
+++ b/src/Pure/PIDE/document.scala	Tue May 29 22:25:59 2018 +0200
@@ -921,6 +921,13 @@
       }
     }
 
+    def node_initialized(version: Version, name: Node.Name): Boolean =
+      name.is_theory &&
+      (version.nodes(name).commands.iterator.find(_.potentially_initialized) match {
+        case None => false
+        case Some(command) => command_states(version, command).headOption.exists(_.initialized)
+      })
+
     def node_consolidated(version: Version, name: Node.Name): Boolean =
       !name.is_theory ||
         version.nodes(name).commands.reverse.iterator.

--- a/src/Pure/PIDE/markup.ML	Tue May 29 20:03:24 2018 +0200
+++ b/src/Pure/PIDE/markup.ML	Tue May 29 22:25:59 2018 +0200
@@ -167,6 +167,7 @@
   val runningN: string val running: T
   val finishedN: string val finished: T
   val failedN: string val failed: T
+  val initializedN: string val initialized: T
   val consolidatedN: string val consolidated: T
   val exec_idN: string
   val initN: string
@@ -580,6 +581,8 @@
 val (runningN, running) = markup_elem "running";
 val (finishedN, finished) = markup_elem "finished";
 val (failedN, failed) = markup_elem "failed";
+
+val (initializedN, initialized) = markup_elem "initialized";
 val (consolidatedN, consolidated) = markup_elem "consolidated";
 
 

--- a/src/Pure/PIDE/markup.scala	Tue May 29 20:03:24 2018 +0200
+++ b/src/Pure/PIDE/markup.scala	Tue May 29 22:25:59 2018 +0200
@@ -426,6 +426,8 @@
   val RUNNING = "running"
   val FINISHED = "finished"
   val FAILED = "failed"
+
+  val INITIALIZED = "initialized"
   val CONSOLIDATED = "consolidated"
 
 

--- a/src/Pure/PIDE/protocol.scala	Tue May 29 20:03:24 2018 +0200
+++ b/src/Pure/PIDE/protocol.scala	Tue May 29 22:25:59 2018 +0200
@@ -142,7 +142,8 @@
   /* node status */
 
   sealed case class Node_Status(
-    unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int, consolidated: Boolean)
+    unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int,
+    initialized: Boolean, consolidated: Boolean)
   {
     def ok: Boolean = failed == 0
     def total: Int = unprocessed + running + warned + failed + finished
@@ -150,7 +151,7 @@
     def json: JSON.Object.T =
       JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
         "running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished,
-        "consolidated" -> consolidated)
+        "initialized" -> initialized, "consolidated" -> consolidated)
   }
 
   def node_status(
@@ -175,9 +176,10 @@
       else if (status.is_finished) finished += 1
       else unprocessed += 1
     }
+    val initialized = state.node_initialized(version, name)
     val consolidated = state.node_consolidated(version, name)
 
-    Node_Status(unprocessed, running, warned, failed, finished, consolidated)
+    Node_Status(unprocessed, running, warned, failed, finished, initialized, consolidated)
   }