# HG changeset patch
# User wenzelm
# Date 1406120446 -7200
# Node ID 335750d989a328a6120fd879666cc35eb24cb11e
# Parent  50ab1db5c0fdcb702cf91a6bbd0b1c324b473d06
clarified display;

diff -r 50ab1db5c0fd -r 335750d989a3 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Jul 23 14:50:20 2014 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Jul 23 15:00:46 2014 +0200
@@ -296,6 +296,9 @@
     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 + (entry: (Node.Name, Node)): Nodes =
     {
       val (name, node) = entry
diff -r 50ab1db5c0fd -r 335750d989a3 src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Wed Jul 23 14:50:20 2014 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Wed Jul 23 15:00:46 2014 +0200
@@ -204,7 +204,7 @@
     val nodes_status1 =
       (nodes_status /: iterator)({ case (status, (name, node)) =>
           if (!name.is_theory || PIDE.resources.loaded_theories(name.theory)) status
-          else if (node.is_empty) status - name
+          else if (snapshot.version.nodes.is_maximal(name) && node.is_empty) status - name
           else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
 
     if (nodes_status != nodes_status1) {