# HG changeset patch
# User wenzelm
# Date 1534593132 -7200
# Node ID 8bb51b3de39f7540a72d6997069b62b0230298f1
# Parent  0626cae56b6f14d83742d5a861a1b315ecf7edcf
trim nodes_status: avoid potential memory leak;

diff -r 0626cae56b6f -r 8bb51b3de39f src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala	Sat Aug 18 13:40:23 2018 +0200
+++ b/src/Pure/PIDE/document_status.scala	Sat Aug 18 13:52:12 2018 +0200
@@ -185,6 +185,9 @@
     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))
+
     override def hashCode: Int = rep.hashCode
     override def equals(that: Any): Boolean =
       that match {
diff -r 0626cae56b6f -r 8bb51b3de39f src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Sat Aug 18 13:40:23 2018 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Sat Aug 18 13:52:12 2018 +0200
@@ -210,7 +210,9 @@
   }
   status.renderer = new Node_Renderer
 
-  private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
+  private def handle_update(
+    restriction: Option[Set[Document.Node.Name]] = None,
+    trim: Boolean = false)
   {
     GUI_Thread.require {}
 
@@ -230,8 +232,11 @@
             }
         })
 
-    if (nodes_status != nodes_status1) {
-      nodes_status = nodes_status1
+    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(_))
     }
   }
@@ -253,7 +258,9 @@
         }
 
       case changed: Session.Commands_Changed =>
-        GUI_Thread.later { handle_update(Some(changed.nodes)) }
+        GUI_Thread.later {
+          handle_update(restriction = Some(changed.nodes), trim = changed.assignment)
+        }
     }
 
   override def init()