src/Pure/PIDE/document.scala
changeset 57619 dcd69422b953
parent 57617 335750d989a3
child 57620 c30ab960875e
     1.1 --- a/src/Pure/PIDE/document.scala	Wed Jul 23 15:11:42 2014 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Wed Jul 23 15:32:05 2014 +0200
     1.3 @@ -296,8 +296,11 @@
     1.4      def apply(name: Node.Name): Node =
     1.5        graph.default_node(name, Node.empty).get_node(name)
     1.6  
     1.7 -    def is_maximal(name: Node.Name): Boolean =
     1.8 -      graph.default_node(name, Node.empty).is_maximal(name)
     1.9 +    def is_hidden(name: Node.Name): Boolean =
    1.10 +    {
    1.11 +      val graph1 = graph.default_node(name, Node.empty)
    1.12 +      graph1.is_maximal(name) && graph1.get_node(name).is_empty
    1.13 +    }
    1.14  
    1.15      def + (entry: (Node.Name, Node)): Nodes =
    1.16      {