# HG changeset patch # User wenzelm # Date 1534588865 -7200 # Node ID a110e7e24e55c61d7f309c9f7a5255fdb3880dd1 # Parent e7e3776385ba52db7d94d75b58349907adaf179a clarified modules; diff -r e7e3776385ba -r a110e7e24e55 src/Pure/PIDE/command.scala --- 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)) diff -r e7e3776385ba -r a110e7e24e55 src/Pure/PIDE/document_status.scala --- /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]) +} diff -r e7e3776385ba -r a110e7e24e55 src/Pure/PIDE/protocol.scala --- 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 = diff -r e7e3776385ba -r a110e7e24e55 src/Pure/PIDE/rendering.scala --- 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) diff -r e7e3776385ba -r a110e7e24e55 src/Pure/Thy/thy_resources.scala --- 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("", _)) diff -r e7e3776385ba -r a110e7e24e55 src/Pure/Tools/dump.scala --- 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) diff -r e7e3776385ba -r a110e7e24e55 src/Pure/build-jars --- 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 diff -r e7e3776385ba -r a110e7e24e55 src/Tools/jEdit/src/theories_dockable.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) } }) diff -r e7e3776385ba -r a110e7e24e55 src/Tools/jEdit/src/timing_dockable.scala --- 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) } })