--- a/src/Pure/PIDE/command.scala Fri Aug 17 21:34:56 2018 +0200
+++ b/src/Pure/PIDE/command.scala Sat Aug 18 12:41:05 2018 +0200
@@ -263,9 +263,24 @@
def initialized: Boolean = status.exists(markup => markup.name == Markup.INITIALIZED)
def consolidated: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATED)
- lazy val maybe_consolidated: Boolean = Protocol.maybe_consolidated(status)
+ lazy val maybe_consolidated: Boolean =
+ {
+ var touched = false
+ var forks = 0
+ var runs = 0
+ for (markup <- status) {
+ markup.name match {
+ case Markup.FORKED => touched = true; forks += 1
+ case Markup.JOINED => forks -= 1
+ case Markup.RUNNING => touched = true; runs += 1
+ case Markup.FINISHED => runs -= 1
+ case _ =>
+ }
+ }
+ touched && forks == 0 && runs == 0
+ }
- lazy val protocol_status: Protocol.Status =
+ lazy val document_status: Document_Status.Command_Status =
{
val warnings =
if (results.iterator.exists(p => Protocol.is_warning(p._2) || Protocol.is_legacy(p._2)))
@@ -275,7 +290,7 @@
if (results.iterator.exists(p => Protocol.is_error(p._2)))
List(Markup(Markup.ERROR, Nil))
else Nil
- Protocol.Status.make((warnings ::: errors ::: status).iterator)
+ Document_Status.Command_Status.make((warnings ::: errors ::: status).iterator)
}
def markup(index: Markup_Index): Markup_Tree = markups(index)
@@ -301,7 +316,7 @@
status: Boolean, chunk_name: Symbol.Text_Chunk.Name, m: Text.Markup): State =
{
val markups1 =
- if (status || Protocol.liberal_status_elements(m.info.name))
+ if (status || Document_Status.Command_Status.liberal_elements(m.info.name))
markups.add(Markup_Index(true, chunk_name), m)
else markups
copy(markups = markups1.add(Markup_Index(false, chunk_name), m))
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/document_status.scala Sat Aug 18 12:41:05 2018 +0200
@@ -0,0 +1,159 @@
+/* Title: Pure/PIDE/document_status.scala
+ Author: Makarius
+
+Document status based on markup information.
+*/
+
+package isabelle
+
+
+object Document_Status
+{
+ /* command status */
+
+ object Command_Status
+ {
+ val proper_elements: Markup.Elements =
+ Markup.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
+ Markup.FINISHED, Markup.FAILED)
+
+ val liberal_elements: Markup.Elements =
+ proper_elements + Markup.WARNING + Markup.LEGACY + Markup.ERROR
+
+ def make(markup_iterator: Iterator[Markup]): Command_Status =
+ {
+ var touched = false
+ var accepted = false
+ var warned = false
+ var failed = false
+ var forks = 0
+ var runs = 0
+ for (markup <- markup_iterator) {
+ markup.name match {
+ case Markup.ACCEPTED => accepted = true
+ case Markup.FORKED => touched = true; forks += 1
+ case Markup.JOINED => forks -= 1
+ case Markup.RUNNING => touched = true; runs += 1
+ case Markup.FINISHED => runs -= 1
+ case Markup.WARNING | Markup.LEGACY => warned = true
+ case Markup.FAILED | Markup.ERROR => failed = true
+ case _ =>
+ }
+ }
+ Command_Status(touched, accepted, warned, failed, forks, runs)
+ }
+
+ val empty = make(Iterator.empty)
+
+ def merge(status_iterator: Iterator[Command_Status]): Command_Status =
+ if (status_iterator.hasNext) {
+ val status0 = status_iterator.next
+ (status0 /: status_iterator)(_ + _)
+ }
+ else empty
+ }
+
+ sealed case class Command_Status(
+ private val touched: Boolean,
+ private val accepted: Boolean,
+ private val warned: Boolean,
+ private val failed: Boolean,
+ forks: Int,
+ runs: Int)
+ {
+ def + (that: Command_Status): Command_Status =
+ Command_Status(
+ touched || that.touched,
+ accepted || that.accepted,
+ warned || that.warned,
+ failed || that.failed,
+ forks + that.forks,
+ runs + that.runs)
+
+ def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0))
+ def is_running: Boolean = runs != 0
+ def is_warned: Boolean = warned
+ def is_failed: Boolean = failed
+ def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0
+ }
+
+
+ /* node status */
+
+ object Node_Status
+ {
+ def make(
+ state: Document.State,
+ version: Document.Version,
+ name: Document.Node.Name): Node_Status =
+ {
+ val node = version.nodes(name)
+
+ var unprocessed = 0
+ var running = 0
+ var warned = 0
+ var failed = 0
+ var finished = 0
+ for (command <- node.commands.iterator) {
+ val states = state.command_states(version, command)
+ val status = Command_Status.merge(states.iterator.map(_.document_status))
+
+ if (status.is_running) running += 1
+ else if (status.is_failed) failed += 1
+ else if (status.is_warned) warned += 1
+ 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, initialized, consolidated)
+ }
+ }
+
+ sealed case class Node_Status(
+ 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
+
+ def json: JSON.Object.T =
+ JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
+ "running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished,
+ "initialized" -> initialized, "consolidated" -> consolidated)
+ }
+
+
+ /* node timing */
+
+ object Node_Timing
+ {
+ val empty: Node_Timing = Node_Timing(0.0, Map.empty)
+
+ def make(
+ state: Document.State,
+ version: Document.Version,
+ node: Document.Node,
+ threshold: Double): Node_Timing =
+ {
+ var total = 0.0
+ var commands = Map.empty[Command, Double]
+ for {
+ command <- node.commands.iterator
+ st <- state.command_states(version, command)
+ } {
+ val command_timing =
+ (0.0 /: st.status)({
+ case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds
+ case (timing, _) => timing
+ })
+ total += command_timing
+ if (command_timing >= threshold) commands += (command -> command_timing)
+ }
+ Node_Timing(total, commands)
+ }
+ }
+
+ sealed case class Node_Timing(total: Double, commands: Map[Command, Double])
+}
--- a/src/Pure/PIDE/protocol.scala Fri Aug 17 21:34:56 2018 +0200
+++ b/src/Pure/PIDE/protocol.scala Sat Aug 18 12:41:05 2018 +0200
@@ -38,95 +38,6 @@
}
- /* consolidation status */
-
- def maybe_consolidated(markups: List[Markup]): Boolean =
- {
- var touched = false
- var forks = 0
- var runs = 0
- for (markup <- markups) {
- markup.name match {
- case Markup.FORKED => touched = true; forks += 1
- case Markup.JOINED => forks -= 1
- case Markup.RUNNING => touched = true; runs += 1
- case Markup.FINISHED => runs -= 1
- case _ =>
- }
- }
- touched && forks == 0 && runs == 0
- }
-
-
- /* command status */
-
- object Status
- {
- def make(markup_iterator: Iterator[Markup]): Status =
- {
- var touched = false
- var accepted = false
- var warned = false
- var failed = false
- var forks = 0
- var runs = 0
- for (markup <- markup_iterator) {
- markup.name match {
- case Markup.ACCEPTED => accepted = true
- case Markup.FORKED => touched = true; forks += 1
- case Markup.JOINED => forks -= 1
- case Markup.RUNNING => touched = true; runs += 1
- case Markup.FINISHED => runs -= 1
- case Markup.WARNING | Markup.LEGACY => warned = true
- case Markup.FAILED | Markup.ERROR => failed = true
- case _ =>
- }
- }
- Status(touched, accepted, warned, failed, forks, runs)
- }
-
- val empty = make(Iterator.empty)
-
- def merge(status_iterator: Iterator[Status]): Status =
- if (status_iterator.hasNext) {
- val status0 = status_iterator.next
- (status0 /: status_iterator)(_ + _)
- }
- else empty
- }
-
- sealed case class Status(
- private val touched: Boolean,
- private val accepted: Boolean,
- private val warned: Boolean,
- private val failed: Boolean,
- forks: Int,
- runs: Int)
- {
- def + (that: Status): Status =
- Status(
- touched || that.touched,
- accepted || that.accepted,
- warned || that.warned,
- failed || that.failed,
- forks + that.forks,
- runs + that.runs)
-
- def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0))
- def is_running: Boolean = runs != 0
- def is_warned: Boolean = warned
- def is_failed: Boolean = failed
- def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0
- }
-
- val proper_status_elements =
- Markup.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
- Markup.FINISHED, Markup.FAILED)
-
- val liberal_status_elements =
- proper_status_elements + Markup.WARNING + Markup.LEGACY + Markup.ERROR
-
-
/* command timing */
object Command_Timing
@@ -159,80 +70,6 @@
}
- /* node status */
-
- sealed case class Node_Status(
- 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
-
- def json: JSON.Object.T =
- JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
- "running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished,
- "initialized" -> initialized, "consolidated" -> consolidated)
- }
-
- def node_status(
- state: Document.State,
- version: Document.Version,
- name: Document.Node.Name): Node_Status =
- {
- val node = version.nodes(name)
-
- var unprocessed = 0
- var running = 0
- var warned = 0
- var failed = 0
- var finished = 0
- for (command <- node.commands.iterator) {
- val states = state.command_states(version, command)
- val status = Status.merge(states.iterator.map(_.protocol_status))
-
- if (status.is_running) running += 1
- else if (status.is_failed) failed += 1
- else if (status.is_warned) warned += 1
- 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, initialized, consolidated)
- }
-
-
- /* node timing */
-
- sealed case class Node_Timing(total: Double, commands: Map[Command, Double])
-
- val empty_node_timing = Node_Timing(0.0, Map.empty)
-
- def node_timing(
- state: Document.State,
- version: Document.Version,
- node: Document.Node,
- threshold: Double): Node_Timing =
- {
- var total = 0.0
- var commands = Map.empty[Command, Double]
- for {
- command <- node.commands.iterator
- st <- state.command_states(version, command)
- } {
- val command_timing =
- (0.0 /: st.status)({
- case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds
- case (timing, _) => timing
- })
- total += command_timing
- if (command_timing >= threshold) commands += (command -> command_timing)
- }
- Node_Timing(total, commands)
- }
-
-
/* result messages */
def is_result(msg: XML.Tree): Boolean =
--- a/src/Pure/PIDE/rendering.scala Fri Aug 17 21:34:56 2018 +0200
+++ b/src/Pure/PIDE/rendering.scala Sat Aug 18 12:41:05 2018 +0200
@@ -182,7 +182,7 @@
Markup.SENDBACK, Markup.JEDIT_ACTION, Markup.SIMP_TRACE_PANEL)
val background_elements =
- Protocol.proper_status_elements + Markup.WRITELN_MESSAGE +
+ Document_Status.Command_Status.proper_elements + Markup.WRITELN_MESSAGE +
Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE +
Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE +
@@ -393,7 +393,7 @@
command_states =>
{
case (((markups, color), Text.Info(_, XML.Elem(markup, _))))
- if markups.nonEmpty && Protocol.proper_status_elements(markup.name) =>
+ if markups.nonEmpty && Document_Status.Command_Status.proper_elements(markup.name) =>
Some((markup :: markups, color))
case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
Some((Nil, Some(Rendering.Color.bad)))
@@ -431,7 +431,7 @@
color <-
(result match {
case (markups, opt_color) if markups.nonEmpty =>
- val status = Protocol.Status.make(markups.iterator)
+ val status = Document_Status.Command_Status.make(markups.iterator)
if (status.is_unprocessed) Some(Rendering.Color.unprocessed1)
else if (status.is_running) Some(Rendering.Color.running1)
else opt_color
@@ -648,13 +648,14 @@
if (snapshot.is_outdated) None
else {
val results =
- snapshot.cumulate[List[Markup]](range, Nil, Protocol.liberal_status_elements, _ =>
- {
- case (status, Text.Info(_, elem)) => Some(elem.markup :: status)
- }, status = true)
+ snapshot.cumulate[List[Markup]](range, Nil, Document_Status.Command_Status.liberal_elements,
+ _ =>
+ {
+ case (status, Text.Info(_, elem)) => Some(elem.markup :: status)
+ }, status = true)
if (results.isEmpty) None
else {
- val status = Protocol.Status.make(results.iterator.flatMap(_.info))
+ val status = Document_Status.Command_Status.make(results.iterator.flatMap(_.info))
if (status.is_running) Some(Rendering.Color.running)
else if (status.is_failed) Some(Rendering.Color.error)
--- a/src/Pure/Thy/thy_resources.scala Fri Aug 17 21:34:56 2018 +0200
+++ b/src/Pure/Thy/thy_resources.scala Sat Aug 18 12:41:05 2018 +0200
@@ -58,7 +58,7 @@
class Theories_Result private[Thy_Resources](
val state: Document.State,
val version: Document.Version,
- val nodes: List[(Document.Node.Name, Protocol.Node_Status)])
+ val nodes: List[(Document.Node.Name, Document_Status.Node_Status)])
{
def node_names: List[Document.Node.Name] = nodes.map(_._1)
def ok: Boolean = nodes.forall({ case (_, st) => st.ok })
@@ -118,7 +118,7 @@
if (beyond_limit || dep_theories.forall(state.node_consolidated(version, _))) {
val nodes =
for (name <- dep_theories)
- yield (name -> Protocol.node_status(state, version, name))
+ yield (name -> Document_Status.Node_Status.make(state, version, name))
try { result.fulfill(new Theories_Result(state, version, nodes)) }
catch { case _: IllegalStateException => }
}
@@ -157,7 +157,8 @@
{
val initialized =
(check_theories -- theories).toList.filter(name =>
- Protocol.node_status(snapshot.state, snapshot.version, name).initialized)
+ Document_Status.Node_Status.make(
+ snapshot.state, snapshot.version, name).initialized)
(initialized, theories ++ initialized)
})
initialized.map(_.theory).sorted.foreach(progress.theory("", _))
--- a/src/Pure/Tools/dump.scala Fri Aug 17 21:34:56 2018 +0200
+++ b/src/Pure/Tools/dump.scala Sat Aug 18 12:41:05 2018 +0200
@@ -17,7 +17,7 @@
deps: Sessions.Deps,
output_dir: Path,
node_name: Document.Node.Name,
- node_status: Protocol.Node_Status,
+ node_status: Document_Status.Node_Status,
snapshot: Document.Snapshot)
{
def write(file_name: Path, bytes: Bytes)
--- a/src/Pure/build-jars Fri Aug 17 21:34:56 2018 +0200
+++ b/src/Pure/build-jars Sat Aug 18 12:41:05 2018 +0200
@@ -93,6 +93,7 @@
PIDE/command_span.scala
PIDE/document.scala
PIDE/document_id.scala
+ PIDE/document_status.scala
PIDE/editor.scala
PIDE/line.scala
PIDE/markup.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala Fri Aug 17 21:34:56 2018 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala Sat Aug 18 12:41:05 2018 +0200
@@ -97,7 +97,7 @@
/* component state -- owned by GUI thread */
- private var nodes_status: Map[Document.Node.Name, Protocol.Node_Status] = Map.empty
+ private var nodes_status: Map[Document.Node.Name, Document_Status.Node_Status] = Map.empty
private var nodes_required: Set[Document.Node.Name] = Document_Model.required_nodes()
private object Overall_Node_Status extends Enumeration
@@ -235,7 +235,7 @@
PIDE.resources.session_base.loaded_theory(name) ||
nodes(name).is_empty) status
else {
- val st = Protocol.node_status(snapshot.state, snapshot.version, name)
+ val st = Document_Status.Node_Status.make(snapshot.state, snapshot.version, name)
status + (name -> st)
}
})
--- a/src/Tools/jEdit/src/timing_dockable.scala Fri Aug 17 21:34:56 2018 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala Sat Aug 18 12:41:05 2018 +0200
@@ -150,7 +150,7 @@
/* component state -- owned by GUI thread */
- private var nodes_timing = Map.empty[Document.Node.Name, Protocol.Node_Timing]
+ private var nodes_timing = Map.empty[Document.Node.Name, Document_Status.Node_Timing]
private def make_entries(): List[Entry] =
{
@@ -161,7 +161,7 @@
case None => Document.Node.Name.empty
case Some(doc_view) => doc_view.model.node_name
}
- val timing = nodes_timing.getOrElse(name, Protocol.empty_node_timing)
+ val timing = nodes_timing.getOrElse(name, Document_Status.Node_Timing.empty)
val theories =
(for ((node_name, node_timing) <- nodes_timing.toList if node_timing.commands.nonEmpty)
@@ -191,7 +191,8 @@
if (PIDE.resources.session_base.loaded_theory(name)) timing1
else {
val node_timing =
- Protocol.node_timing(snapshot.state, snapshot.version, node, timing_threshold)
+ Document_Status.Node_Timing.make(
+ snapshot.state, snapshot.version, node, timing_threshold)
timing1 + (name -> node_timing)
}
})