# HG changeset patch # User wenzelm # Date 1536064831 -7200 # Node ID 58525b08eed16bf23afc43a210f3dedb1144eca1 # Parent 8414bbd7bb46e5fbe76a0ba72ea6ddb5f673e121 clarified Nodes_Status; tuned messages; diff -r 8414bbd7bb46 -r 58525b08eed1 src/Pure/PIDE/document_status.scala --- 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 diff -r 8414bbd7bb46 -r 58525b08eed1 src/Pure/System/progress.scala --- 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)) } diff -r 8414bbd7bb46 -r 58525b08eed1 src/Pure/Thy/thy_resources.scala --- 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() } } diff -r 8414bbd7bb46 -r 58525b08eed1 src/Pure/Tools/server.scala --- 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)) } diff -r 8414bbd7bb46 -r 58525b08eed1 src/Tools/jEdit/src/theories_dockable.scala --- 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) }