# HG changeset patch
# User wenzelm
# Date 1550438102 -3600
# Node ID 5f160df596c16f0937639798536c60149826dd81
# Parent  ce4842d2d15066722a97f2d97c87767072f651d4
clarified Node_Status vs. is_suppressed, e.g. relevant for purged nodes in Theories_Dockable after 0626cae56b6f;

diff -r ce4842d2d150 -r 5f160df596c1 src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala	Sun Feb 17 19:31:04 2019 +0100
+++ b/src/Pure/PIDE/document_status.scala	Sun Feb 17 22:15:02 2019 +0100
@@ -230,9 +230,12 @@
     def apply(name: Document.Node.Name): Node_Status = rep(name)
     def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name)
 
-    def present: List[(Document.Node.Name, Node_Status)] =
-      for { name <- nodes.topological_order; node_status <- get(name) }
-        yield (name, node_status)
+    def present(snapshot: Document.Snapshot): List[(Document.Node.Name, Node_Status)] =
+      (for {
+        name <- nodes.topological_order.iterator
+        node_status <- get(name)
+        if !snapshot.version.nodes.is_suppressed(name)
+      } yield (name, node_status)).toList
 
     def quasi_consolidated(name: Document.Node.Name): Boolean =
       rep.get(name) match {
@@ -258,10 +261,7 @@
       val update_iterator =
         for {
           name <- domain.getOrElse(nodes1.domain).iterator
-          if !resources.is_hidden(name) &&
-              !resources.session_base.loaded_theory(name) &&
-              !nodes1.is_suppressed(name) &&
-              !nodes1(name).is_empty
+          if !resources.is_hidden(name) && !resources.session_base.loaded_theory(name)
           st = Document_Status.Node_Status.make(state, version, name)
           if !rep.isDefinedAt(name) || rep(name) != st
         } yield (name -> st)
diff -r ce4842d2d150 -r 5f160df596c1 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Sun Feb 17 19:31:04 2019 +0100
+++ b/src/Pure/PIDE/headless.scala	Sun Feb 17 22:15:02 2019 +0100
@@ -204,7 +204,7 @@
       {
         val delay_nodes_status =
           Standard_Thread.delay_first(nodes_status_delay max Time.zero) {
-            progress.nodes_status(use_theories_state.value.nodes_status)
+            progress.nodes_status(session.snapshot(), use_theories_state.value.nodes_status)
           }
 
         val delay_commit_clean =
@@ -239,7 +239,7 @@
 
                     val theory_progress =
                       (for {
-                        (name, node_status) <- nodes_status1.present.iterator
+                        (name, node_status) <- nodes_status1.present(snapshot).iterator
                         if changed.nodes.contains(name) && !st.already_committed.isDefinedAt(name)
                         p1 = node_status.percentage
                         if p1 > 0 && Some(p1) != st.nodes_status.get(name).map(_.percentage)
diff -r ce4842d2d150 -r 5f160df596c1 src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Sun Feb 17 19:31:04 2019 +0100
+++ b/src/Pure/System/progress.scala	Sun Feb 17 22:15:02 2019 +0100
@@ -28,7 +28,7 @@
   def echo(msg: String) {}
   def echo_if(cond: Boolean, msg: String) { if (cond) echo(msg) }
   def theory(theory: Progress.Theory) {}
-  def nodes_status(nodes_status: Document_Status.Nodes_Status) {}
+  def nodes_status(snapshot: Document.Snapshot, 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 ce4842d2d150 -r 5f160df596c1 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Sun Feb 17 19:31:04 2019 +0100
+++ b/src/Pure/Tools/server.scala	Sun Feb 17 22:15:02 2019 +0100
@@ -267,10 +267,11 @@
       context.writeln(theory.message, entries ::: more.toList:_*)
     }
 
-    override def nodes_status(nodes_status: Document_Status.Nodes_Status)
+    override def nodes_status(
+      snapshot: Document.Snapshot, nodes_status: Document_Status.Nodes_Status)
     {
       val json =
-        for ((name, node_status) <- nodes_status.present)
+        for ((name, node_status) <- nodes_status.present(snapshot))
           yield name.json + ("status" -> nodes_status(name).json)
       context.notify(JSON.Object(Markup.KIND -> Markup.NODES_STATUS, Markup.NODES_STATUS -> json))
     }
diff -r ce4842d2d150 -r 5f160df596c1 src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Sun Feb 17 19:31:04 2019 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Sun Feb 17 22:15:02 2019 +0100
@@ -221,7 +221,7 @@
         PIDE.resources, snapshot.state, snapshot.version, domain = domain, trim = trim)
 
     nodes_status = nodes_status1
-    if (nodes_status_changed) status.listData = nodes_status1.present.map(_._1)
+    if (nodes_status_changed) status.listData = nodes_status1.present(snapshot).map(_._1)
   }