clarified Node_Status vs. is_suppressed, e.g. relevant for purged nodes in Theories_Dockable after 0626cae56b6f;
authorwenzelm
Sun Feb 17 22:15:02 2019 +0100 (6 months ago ago)
changeset 699975f160df596c1
parent 69996 ce4842d2d150
child 69998 60d0ee8f2ddb
clarified Node_Status vs. is_suppressed, e.g. relevant for purged nodes in Theories_Dockable after 0626cae56b6f;
src/Pure/PIDE/document_status.scala
src/Pure/PIDE/headless.scala
src/Pure/System/progress.scala
src/Pure/Tools/server.scala
src/Tools/jEdit/src/theories_dockable.scala
     1.1 --- a/src/Pure/PIDE/document_status.scala	Sun Feb 17 19:31:04 2019 +0100
     1.2 +++ b/src/Pure/PIDE/document_status.scala	Sun Feb 17 22:15:02 2019 +0100
     1.3 @@ -230,9 +230,12 @@
     1.4      def apply(name: Document.Node.Name): Node_Status = rep(name)
     1.5      def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name)
     1.6  
     1.7 -    def present: List[(Document.Node.Name, Node_Status)] =
     1.8 -      for { name <- nodes.topological_order; node_status <- get(name) }
     1.9 -        yield (name, node_status)
    1.10 +    def present(snapshot: Document.Snapshot): List[(Document.Node.Name, Node_Status)] =
    1.11 +      (for {
    1.12 +        name <- nodes.topological_order.iterator
    1.13 +        node_status <- get(name)
    1.14 +        if !snapshot.version.nodes.is_suppressed(name)
    1.15 +      } yield (name, node_status)).toList
    1.16  
    1.17      def quasi_consolidated(name: Document.Node.Name): Boolean =
    1.18        rep.get(name) match {
    1.19 @@ -258,10 +261,7 @@
    1.20        val update_iterator =
    1.21          for {
    1.22            name <- domain.getOrElse(nodes1.domain).iterator
    1.23 -          if !resources.is_hidden(name) &&
    1.24 -              !resources.session_base.loaded_theory(name) &&
    1.25 -              !nodes1.is_suppressed(name) &&
    1.26 -              !nodes1(name).is_empty
    1.27 +          if !resources.is_hidden(name) && !resources.session_base.loaded_theory(name)
    1.28            st = Document_Status.Node_Status.make(state, version, name)
    1.29            if !rep.isDefinedAt(name) || rep(name) != st
    1.30          } yield (name -> st)
     2.1 --- a/src/Pure/PIDE/headless.scala	Sun Feb 17 19:31:04 2019 +0100
     2.2 +++ b/src/Pure/PIDE/headless.scala	Sun Feb 17 22:15:02 2019 +0100
     2.3 @@ -204,7 +204,7 @@
     2.4        {
     2.5          val delay_nodes_status =
     2.6            Standard_Thread.delay_first(nodes_status_delay max Time.zero) {
     2.7 -            progress.nodes_status(use_theories_state.value.nodes_status)
     2.8 +            progress.nodes_status(session.snapshot(), use_theories_state.value.nodes_status)
     2.9            }
    2.10  
    2.11          val delay_commit_clean =
    2.12 @@ -239,7 +239,7 @@
    2.13  
    2.14                      val theory_progress =
    2.15                        (for {
    2.16 -                        (name, node_status) <- nodes_status1.present.iterator
    2.17 +                        (name, node_status) <- nodes_status1.present(snapshot).iterator
    2.18                          if changed.nodes.contains(name) && !st.already_committed.isDefinedAt(name)
    2.19                          p1 = node_status.percentage
    2.20                          if p1 > 0 && Some(p1) != st.nodes_status.get(name).map(_.percentage)
     3.1 --- a/src/Pure/System/progress.scala	Sun Feb 17 19:31:04 2019 +0100
     3.2 +++ b/src/Pure/System/progress.scala	Sun Feb 17 22:15:02 2019 +0100
     3.3 @@ -28,7 +28,7 @@
     3.4    def echo(msg: String) {}
     3.5    def echo_if(cond: Boolean, msg: String) { if (cond) echo(msg) }
     3.6    def theory(theory: Progress.Theory) {}
     3.7 -  def nodes_status(nodes_status: Document_Status.Nodes_Status) {}
     3.8 +  def nodes_status(snapshot: Document.Snapshot, nodes_status: Document_Status.Nodes_Status) {}
     3.9  
    3.10    def echo_warning(msg: String) { echo(Output.warning_text(msg)) }
    3.11    def echo_error_message(msg: String) { echo(Output.error_message_text(msg)) }
     4.1 --- a/src/Pure/Tools/server.scala	Sun Feb 17 19:31:04 2019 +0100
     4.2 +++ b/src/Pure/Tools/server.scala	Sun Feb 17 22:15:02 2019 +0100
     4.3 @@ -267,10 +267,11 @@
     4.4        context.writeln(theory.message, entries ::: more.toList:_*)
     4.5      }
     4.6  
     4.7 -    override def nodes_status(nodes_status: Document_Status.Nodes_Status)
     4.8 +    override def nodes_status(
     4.9 +      snapshot: Document.Snapshot, nodes_status: Document_Status.Nodes_Status)
    4.10      {
    4.11        val json =
    4.12 -        for ((name, node_status) <- nodes_status.present)
    4.13 +        for ((name, node_status) <- nodes_status.present(snapshot))
    4.14            yield name.json + ("status" -> nodes_status(name).json)
    4.15        context.notify(JSON.Object(Markup.KIND -> Markup.NODES_STATUS, Markup.NODES_STATUS -> json))
    4.16      }
     5.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Sun Feb 17 19:31:04 2019 +0100
     5.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Sun Feb 17 22:15:02 2019 +0100
     5.3 @@ -221,7 +221,7 @@
     5.4          PIDE.resources, snapshot.state, snapshot.version, domain = domain, trim = trim)
     5.5  
     5.6      nodes_status = nodes_status1
     5.7 -    if (nodes_status_changed) status.listData = nodes_status1.present.map(_._1)
     5.8 +    if (nodes_status_changed) status.listData = nodes_status1.present(snapshot).map(_._1)
     5.9    }
    5.10  
    5.11