# HG changeset patch
# User wenzelm
# Date 1534596162 -7200
# Node ID b523e903d6e408a6171e6319954492ebddb021ea
# Parent  3c5857c6bc5b70fb8315fefc8a04528ecc40a85c
clarified signature;

diff -r 3c5857c6bc5b -r b523e903d6e4 src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala	Sat Aug 18 14:35:48 2018 +0200
+++ b/src/Pure/PIDE/document_status.scala	Sat Aug 18 14:42:42 2018 +0200
@@ -172,7 +172,6 @@
 
   final class Nodes_Status private(private val rep: Map[Document.Node.Name, Node_Status])
   {
-    def defined(name: Document.Node.Name): Boolean = rep.isDefinedAt(name)
     def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name)
 
     def overall_node_status(name: Document.Node.Name): Overall_Node_Status.Value =
@@ -187,7 +186,7 @@
       state: Document.State,
       version: Document.Version,
       restriction: Option[Set[Document.Node.Name]],
-      trim: Boolean): Nodes_Status =
+      trim: Boolean): Option[(Nodes_Status, List[Document.Node.Name])] =
     {
       val nodes = version.nodes
       val update_iterator =
@@ -202,7 +201,9 @@
         } yield (name -> st)
       val rep1 = rep ++ update_iterator
       val rep2 = if (trim) rep1 -- rep1.keysIterator.filterNot(nodes.domain) else rep1
-      new Nodes_Status(rep2)
+
+      if (rep == rep2) None
+      else Some(new Nodes_Status(rep2), version.nodes.topological_order.filter(rep2.keySet))
     }
 
     override def hashCode: Int = rep.hashCode
diff -r 3c5857c6bc5b -r b523e903d6e4 src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Sat Aug 18 14:35:48 2018 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Sat Aug 18 14:42:42 2018 +0200
@@ -218,13 +218,13 @@
 
     val snapshot = PIDE.session.snapshot()
 
-    val nodes_status1 =
-      nodes_status.update(
-        PIDE.resources.session_base, snapshot.state, snapshot.version, restriction, trim)
-
-    if (nodes_status != nodes_status1) {
+    for {
+      (nodes_status1, nodes_list) <-
+        nodes_status.update(
+          PIDE.resources.session_base, snapshot.state, snapshot.version, restriction, trim)
+    } {
       nodes_status = nodes_status1
-      status.listData = snapshot.version.nodes.topological_order.filter(nodes_status.defined(_))
+      status.listData = nodes_list
     }
   }