# HG changeset patch
# User wenzelm
# Date 1534592423 -7200
# Node ID 0626cae56b6f14d83742d5a861a1b315ecf7edcf
# Parent  4247e91fa21deee4070b26ac6dcc8264552694ae
simplified (cf. dcd69422b953);

diff -r 4247e91fa21d -r 0626cae56b6f src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala	Sat Aug 18 13:33:40 2018 +0200
+++ b/src/Pure/PIDE/document_status.scala	Sat Aug 18 13:40:23 2018 +0200
@@ -172,8 +172,6 @@
 
   final class Nodes_Status private(private val rep: Map[Document.Node.Name, Node_Status])
   {
-    def keys_iterator: Iterator[Document.Node.Name] = rep.keysIterator
-
     def defined(name: Document.Node.Name): Boolean = rep.isDefinedAt(name)
     def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name)
 
@@ -187,9 +185,6 @@
     def + (entry: (Document.Node.Name, Node_Status)): Nodes_Status =
       new Nodes_Status(rep + entry)
 
-    def - (name: Document.Node.Name): Nodes_Status =
-      new Nodes_Status(rep - name)
-
     override def hashCode: Int = rep.hashCode
     override def equals(that: Any): Boolean =
       that match {
diff -r 4247e91fa21d -r 0626cae56b6f src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Sat Aug 18 13:33:40 2018 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Sat Aug 18 13:40:23 2018 +0200
@@ -222,6 +222,7 @@
         { case (status, name) =>
             if (PIDE.resources.is_hidden(name) ||
                 PIDE.resources.session_base.loaded_theory(name) ||
+                nodes.is_suppressed(name) ||
                 nodes(name).is_empty) status
             else {
               val st = Document_Status.Node_Status.make(snapshot.state, snapshot.version, name)
@@ -229,11 +230,8 @@
             }
         })
 
-    val nodes_status2 =
-      (nodes_status1 /: nodes_status1.keys_iterator.filter(nodes.is_suppressed(_)))(_ - _)
-
-    if (nodes_status != nodes_status2) {
-      nodes_status = nodes_status2
+    if (nodes_status != nodes_status1) {
+      nodes_status = nodes_status1
       status.listData = nodes.topological_order.filter(nodes_status.defined(_))
     }
   }