# HG changeset patch
# User wenzelm
# Date 1534595748 -7200
# Node ID 3c5857c6bc5b70fb8315fefc8a04528ecc40a85c
# Parent  8750edd967cef00afe3562dd03dbd7bf76e97730
clarified signature;

diff -r 8750edd967ce -r 3c5857c6bc5b src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala	Sat Aug 18 14:16:24 2018 +0200
+++ b/src/Pure/PIDE/document_status.scala	Sat Aug 18 14:35:48 2018 +0200
@@ -182,11 +182,28 @@
         case _ => Overall_Node_Status.pending
       }
 
-    def + (entry: (Document.Node.Name, Node_Status)): Nodes_Status =
-      new Nodes_Status(rep + entry)
-
-    def restrict(domain: Set[Document.Node.Name]): Nodes_Status =
-      new Nodes_Status(rep -- rep.keysIterator.filterNot(domain))
+    def update(
+      session_base: Sessions.Base,
+      state: Document.State,
+      version: Document.Version,
+      restriction: Option[Set[Document.Node.Name]],
+      trim: Boolean): Nodes_Status =
+    {
+      val nodes = version.nodes
+      val update_iterator =
+        for {
+          name <- restriction.getOrElse(nodes.domain).iterator
+          if !Sessions.is_hidden(name) &&
+              !session_base.loaded_theory(name) &&
+              !nodes.is_suppressed(name) &&
+              !nodes(name).is_empty
+          st = Document_Status.Node_Status.make(state, version, name)
+          if !rep.isDefinedAt(name) || rep(name) != st
+        } yield (name -> st)
+      val rep1 = rep ++ update_iterator
+      val rep2 = if (trim) rep1 -- rep1.keysIterator.filterNot(nodes.domain) else rep1
+      new Nodes_Status(rep2)
+    }
 
     override def hashCode: Int = rep.hashCode
     override def equals(that: Any): Boolean =
diff -r 8750edd967ce -r 3c5857c6bc5b src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Sat Aug 18 14:16:24 2018 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Sat Aug 18 14:35:48 2018 +0200
@@ -217,27 +217,14 @@
     GUI_Thread.require {}
 
     val snapshot = PIDE.session.snapshot()
-    val nodes = snapshot.version.nodes
 
     val nodes_status1 =
-      (nodes_status /: (restriction.getOrElse(nodes.domain).iterator))(
-        { case (status, name) =>
-            if (Sessions.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)
-              status + (name -> st)
-            }
-        })
+      nodes_status.update(
+        PIDE.resources.session_base, snapshot.state, snapshot.version, restriction, trim)
 
-    val nodes_status2 =
-      if (trim) nodes_status1.restrict(nodes.domain) else nodes_status1
-
-    if (nodes_status != nodes_status2) {
-      nodes_status = nodes_status2
-      status.listData = nodes.topological_order.filter(nodes_status.defined(_))
+    if (nodes_status != nodes_status1) {
+      nodes_status = nodes_status1
+      status.listData = snapshot.version.nodes.topological_order.filter(nodes_status.defined(_))
     }
   }