# HG changeset patch
# User wenzelm
# Date 1406122325 -7200
# Node ID dcd69422b9535f017d1bd9c4d444f2ce255b4757
# Parent  d762318438c361ae910276b8f8c53935b993a771
clarified display;

diff -r d762318438c3 -r dcd69422b953 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Jul 23 15:11:42 2014 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Jul 23 15:32:05 2014 +0200
@@ -296,8 +296,11 @@
     def apply(name: Node.Name): Node =
       graph.default_node(name, Node.empty).get_node(name)
 
-    def is_maximal(name: Node.Name): Boolean =
-      graph.default_node(name, Node.empty).is_maximal(name)
+    def is_hidden(name: Node.Name): Boolean =
+    {
+      val graph1 = graph.default_node(name, Node.empty)
+      graph1.is_maximal(name) && graph1.get_node(name).is_empty
+    }
 
     def + (entry: (Node.Name, Node)): Nodes =
     {
diff -r d762318438c3 -r dcd69422b953 src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Wed Jul 23 15:11:42 2014 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Wed Jul 23 15:32:05 2014 +0200
@@ -195,23 +195,25 @@
     GUI_Thread.require {}
 
     val snapshot = PIDE.session.snapshot()
+    val nodes = snapshot.version.nodes
 
     val iterator =
       restriction match {
-        case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
-        case None => snapshot.version.nodes.iterator
+        case Some(names) => names.iterator.map(name => (name, nodes(name)))
+        case None => nodes.iterator
       }
     val nodes_status1 =
       (nodes_status /: iterator)({ case (status, (name, node)) =>
-          if (!name.is_theory || PIDE.resources.loaded_theories(name.theory)) status
-          else if (snapshot.version.nodes.is_maximal(name) && node.is_empty) status - name
+          if (!name.is_theory || PIDE.resources.loaded_theories(name.theory) || node.is_empty)
+            status
           else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
 
-    if (nodes_status != nodes_status1) {
-      nodes_status = nodes_status1
-      status.listData =
-        snapshot.version.nodes.topological_order.filter(
-          (name: Document.Node.Name) => nodes_status.isDefinedAt(name))
+    val nodes_status2 =
+      nodes_status1 -- nodes_status1.keysIterator.filter(nodes.is_hidden(_))
+
+    if (nodes_status != nodes_status2) {
+      nodes_status = nodes_status2
+      status.listData = nodes.topological_order.filter(nodes_status.isDefinedAt(_))
     }
   }