# HG changeset patch # User wenzelm # Date 1527625559 -7200 # Node ID bf733673198191d80f1018272557b3ab93121075 # Parent 100f018096c89ced609700e4718d8f9a6d5f52c9 more node status information; diff -r 100f018096c8 -r bf7336731981 src/Doc/System/Server.thy --- 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>\HOL-ex.Seq\). \<^item> \<^bold>\type\ \node_status = {ok: bool, total: int, unprocessed: int, running: - int, warned: int, failed: int, finished: int, consolidated: bool}\ - represents a formal theory node status of the PIDE document model. Fields - \total\, \unprocessed\, \running\, \warned\, \failed\, \finished\ account - for individual commands within a theory node; \ok\ is an abstraction for - \failed = 0\. The \consolidated\ flag indicates whether the outermost theory - command structure has finished (or failed) and the final \<^theory_text>\end\ command has - been checked. + int, warned: int, failed: int, finished: int, initialized: bool, + consolidated: bool}\ represents a formal theory node status of the PIDE + document model. Fields \total\, \unprocessed\, \running\, \warned\, + \failed\, \finished\ account for individual commands within a theory node; + \ok\ is an abstraction for \failed = 0\. The \initialized\ flag indicates + that the initial \<^theory_text>\theory\ command has been processed. The \consolidated\ + flag indicates whether the outermost theory command structure has finished + (or failed) and the final \<^theory_text>\end\ command has been checked. \ diff -r 100f018096c8 -r bf7336731981 src/Pure/PIDE/command.scala --- 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 */ diff -r 100f018096c8 -r bf7336731981 src/Pure/PIDE/document.ML --- 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 diff -r 100f018096c8 -r bf7336731981 src/Pure/PIDE/document.scala --- 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. diff -r 100f018096c8 -r bf7336731981 src/Pure/PIDE/markup.ML --- 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"; diff -r 100f018096c8 -r bf7336731981 src/Pure/PIDE/markup.scala --- 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" diff -r 100f018096c8 -r bf7336731981 src/Pure/PIDE/protocol.scala --- 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) }