--- 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 =
{