# HG changeset patch
# User wenzelm
# Date 1550501826 -3600
# Node ID 60d0ee8f2ddb93777845226d176ad3cef6c79908
# Parent  5f160df596c16f0937639798536c60149826dd81
more robust: avoid potentially unrelated snapshot for the sake of is_suppressed;

diff -r 5f160df596c1 -r 60d0ee8f2ddb src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala	Sun Feb 17 22:15:02 2019 +0100
+++ b/src/Pure/PIDE/document_status.scala	Mon Feb 18 15:57:06 2019 +0100
@@ -134,6 +134,7 @@
       val consolidated = state.node_consolidated(version, name)
 
       Node_Status(
+        is_suppressed = version.nodes.is_suppressed(name),
         unprocessed = unprocessed,
         running = running,
         warned = warned,
@@ -148,6 +149,7 @@
   }
 
   sealed case class Node_Status(
+    is_suppressed: Boolean,
     unprocessed: Int,
     running: Int,
     warned: Int,
@@ -230,11 +232,10 @@
     def apply(name: Document.Node.Name): Node_Status = rep(name)
     def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name)
 
-    def present(snapshot: Document.Snapshot): List[(Document.Node.Name, Node_Status)] =
+    def present: 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 =
diff -r 5f160df596c1 -r 60d0ee8f2ddb src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Sun Feb 17 22:15:02 2019 +0100
+++ b/src/Pure/PIDE/headless.scala	Mon Feb 18 15:57:06 2019 +0100
@@ -204,7 +204,7 @@
       {
         val delay_nodes_status =
           Standard_Thread.delay_first(nodes_status_delay max Time.zero) {
-            progress.nodes_status(session.snapshot(), use_theories_state.value.nodes_status)
+            progress.nodes_status(use_theories_state.value.nodes_status)
           }
 
         val delay_commit_clean =
@@ -239,7 +239,7 @@
 
                     val theory_progress =
                       (for {
-                        (name, node_status) <- nodes_status1.present(snapshot).iterator
+                        (name, node_status) <- nodes_status1.present.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 5f160df596c1 -r 60d0ee8f2ddb src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Sun Feb 17 22:15:02 2019 +0100
+++ b/src/Pure/System/progress.scala	Mon Feb 18 15:57:06 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(snapshot: Document.Snapshot, nodes_status: Document_Status.Nodes_Status) {}
+  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 5f160df596c1 -r 60d0ee8f2ddb src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Sun Feb 17 22:15:02 2019 +0100
+++ b/src/Pure/Tools/server.scala	Mon Feb 18 15:57:06 2019 +0100
@@ -267,11 +267,10 @@
       context.writeln(theory.message, entries ::: more.toList:_*)
     }
 
-    override def nodes_status(
-      snapshot: Document.Snapshot, nodes_status: Document_Status.Nodes_Status)
+    override def nodes_status(nodes_status: Document_Status.Nodes_Status)
     {
       val json =
-        for ((name, node_status) <- nodes_status.present(snapshot))
+        for ((name, node_status) <- nodes_status.present)
           yield name.json + ("status" -> nodes_status(name).json)
       context.notify(JSON.Object(Markup.KIND -> Markup.NODES_STATUS, Markup.NODES_STATUS -> json))
     }
diff -r 5f160df596c1 -r 60d0ee8f2ddb src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Sun Feb 17 22:15:02 2019 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Feb 18 15:57:06 2019 +0100
@@ -221,7 +221,11 @@
         PIDE.resources, snapshot.state, snapshot.version, domain = domain, trim = trim)
 
     nodes_status = nodes_status1
-    if (nodes_status_changed) status.listData = nodes_status1.present(snapshot).map(_._1)
+    if (nodes_status_changed) {
+      status.listData =
+        (for { (name, node_status) <- nodes_status1.present.iterator if !node_status.is_suppressed }
+          yield name).toList
+    }
   }