--- a/src/Pure/PIDE/document_status.scala Tue Sep 04 08:40:53 2018 +0200
+++ b/src/Pure/PIDE/document_status.scala Tue Sep 04 14:40:31 2018 +0200
@@ -219,18 +219,21 @@
object Nodes_Status
{
- val empty: Nodes_Status = new Nodes_Status(Map.empty)
-
- type Update = (Nodes_Status, List[Document.Node.Name])
- val empty_update: Update = (empty, Nil)
+ val empty: Nodes_Status = new Nodes_Status(Map.empty, Document.Nodes.empty)
}
- final class Nodes_Status private(private val rep: Map[Document.Node.Name, Node_Status])
+ final class Nodes_Status private(
+ private val rep: Map[Document.Node.Name, Node_Status],
+ nodes: Document.Nodes)
{
def is_empty: Boolean = rep.isEmpty
def apply(name: Document.Node.Name): Node_Status = rep(name)
def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name)
+ def dest: List[(Document.Node.Name, Node_Status)] =
+ for { name <- nodes.topological_order; node_status <- get(name) }
+ yield (name, node_status)
+
def quasi_consolidated(name: Document.Node.Name): Boolean =
rep.get(name) match {
case Some(st) => st.quasi_consolidated
@@ -249,24 +252,23 @@
state: Document.State,
version: Document.Version,
domain: Option[Set[Document.Node.Name]] = None,
- trim: Boolean = false): Option[Nodes_Status.Update] =
+ trim: Boolean = false): (Boolean, Nodes_Status) =
{
- val nodes = version.nodes
+ val nodes1 = version.nodes
val update_iterator =
for {
- name <- domain.getOrElse(nodes.domain).iterator
+ name <- domain.getOrElse(nodes1.domain).iterator
if !Sessions.is_hidden(name) &&
!session_base.loaded_theory(name) &&
- !nodes.is_suppressed(name) &&
- !nodes(name).is_empty
+ !nodes1.is_suppressed(name) &&
+ !nodes1(name).is_empty
st = Document_Status.Node_Status.make(state, version, name)
if !rep.isDefinedAt(name) || rep(name) != st
} yield (name -> st)
val rep1 = rep ++ update_iterator
- val rep2 = if (trim) rep1 -- rep1.keysIterator.filterNot(nodes.domain) else rep1
+ val rep2 = if (trim) rep1 -- rep1.keysIterator.filterNot(nodes1.domain) else rep1
- if (rep == rep2) None
- else Some(new Nodes_Status(rep2), version.nodes.topological_order.filter(rep2.keySet))
+ (rep != rep2, new Nodes_Status(rep2, nodes1))
}
override def hashCode: Int = rep.hashCode
--- a/src/Pure/System/progress.scala Tue Sep 04 08:40:53 2018 +0200
+++ b/src/Pure/System/progress.scala Tue Sep 04 14:40:31 2018 +0200
@@ -22,7 +22,7 @@
def echo_if(cond: Boolean, msg: String) { if (cond) echo(msg) }
def theory(session: String, theory: String) {}
def theory_percentage(session: String, theory: String, percentage: Int) {}
- def nodes_status(nodes_status: Document_Status.Nodes_Status, names: List[Document.Node.Name]) {}
+ def nodes_status(nodes_status: Document_Status.Nodes_Status) {}
def echo_warning(msg: String) { echo(Output.warning_text(msg)) }
def echo_error_message(msg: String) { echo(Output.error_message_text(msg)) }
--- a/src/Pure/Thy/thy_resources.scala Tue Sep 04 08:40:53 2018 +0200
+++ b/src/Pure/Thy/thy_resources.scala Tue Sep 04 14:40:31 2018 +0200
@@ -115,7 +115,7 @@
}
val dep_theories_set = dep_theories.toSet
- val nodes_status_update = Synchronized(Document_Status.Nodes_Status.empty_update)
+ val current_nodes_status = Synchronized(Document_Status.Nodes_Status.empty)
val result = Future.promise[Theories_Result]
@@ -127,7 +127,7 @@
if (beyond_limit ||
dep_theories.forall(name =>
state.node_consolidated(version, name) ||
- nodes_status_update.value._1.quasi_consolidated(name)))
+ current_nodes_status.value.quasi_consolidated(name)))
{
val nodes =
for (name <- dep_theories)
@@ -156,8 +156,7 @@
val delay_nodes_status =
Standard_Thread.delay_first(nodes_status_delay max Time.zero) {
- val (nodes_status, names) = nodes_status_update.value
- progress.nodes_status(nodes_status, names)
+ progress.nodes_status(current_nodes_status.value)
}
val consumer =
@@ -168,29 +167,31 @@
val state = snapshot.state
val version = snapshot.version
- nodes_status_update.change(
- { case upd @ (nodes_status, _) =>
+ val theory_percentages =
+ current_nodes_status.change_result(nodes_status =>
+ {
val domain =
if (nodes_status.is_empty) dep_theories_set
else changed.nodes.iterator.filter(dep_theories_set).toSet
- val upd1 @ (nodes_status1, names1) =
+ val (nodes_status_changed, nodes_status1) =
nodes_status.update(resources.session_base, state, version,
- domain = Some(domain), trim = changed.assignment).getOrElse(upd)
+ domain = Some(domain), trim = changed.assignment)
- for {
- name <- names1.iterator if changed.nodes.contains(name)
- p = nodes_status.get(name).map(_.percentage)
- p1 = nodes_status1.get(name).map(_.percentage)
- if p != p1 && p1.isDefined && p1.get > 0
- } progress.theory_percentage("", name.theory, p1.get)
-
- if (nodes_status_delay >= Time.zero && upd != upd1) {
+ if (nodes_status_delay >= Time.zero && nodes_status_changed) {
delay_nodes_status.invoke
}
- upd1
- })
+ val progress_percentage =
+ for {
+ (name, node_status) <- nodes_status1.dest.iterator
+ if changed.nodes.contains(name)
+ p1 = node_status.percentage
+ if p1 > 0 && Some(p1) != nodes_status.get(name).map(_.percentage)
+ } yield (name.theory, p1)
+
+ (progress_percentage, nodes_status1)
+ })
val check_theories =
(for {
@@ -210,6 +211,9 @@
initialized.map(_.theory).sorted.foreach(progress.theory("", _))
}
+ for ((theory, percentage) <- theory_percentages)
+ progress.theory_percentage("", theory, percentage)
+
check_state()
}
}
--- a/src/Pure/Tools/server.scala Tue Sep 04 08:40:53 2018 +0200
+++ b/src/Pure/Tools/server.scala Tue Sep 04 14:40:31 2018 +0200
@@ -273,10 +273,11 @@
context.writeln(Progress.theory_message(session, theory),
(List("session" -> session, "theory" -> theory) ::: more.toList):_*)
- override def nodes_status(
- nodes_status: Document_Status.Nodes_Status, names: List[Document.Node.Name])
+ override def nodes_status(nodes_status: Document_Status.Nodes_Status)
{
- val json = names.map(name => name.json + ("status" -> nodes_status(name).json))
+ val json =
+ for ((name, node_status) <- nodes_status.dest)
+ yield name.json + ("status" -> nodes_status(name).json)
context.notify(JSON.Object(Markup.KIND -> Markup.NODES_STATUS, Markup.NODES_STATUS -> json))
}
--- a/src/Tools/jEdit/src/theories_dockable.scala Tue Sep 04 08:40:53 2018 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala Tue Sep 04 14:40:31 2018 +0200
@@ -217,11 +217,12 @@
val session_base = PIDE.resources.session_base
val snapshot = PIDE.session.snapshot()
- for {
- (nodes_status1, nodes_list1) <-
- nodes_status.update(
- session_base, snapshot.state, snapshot.version, domain = domain, trim = trim)
- } { nodes_status = nodes_status1; status.listData = nodes_list1 }
+ val (nodes_status_changed, nodes_status1) =
+ nodes_status.update(
+ session_base, snapshot.state, snapshot.version, domain = domain, trim = trim)
+
+ nodes_status = nodes_status1
+ if (nodes_status_changed) status.listData = nodes_status1.dest.map(_._1)
}