clarified display;
authorwenzelm
Wed Jul 23 15:00:46 2014 +0200 (2014-07-23)
changeset 57617335750d989a3
parent 57616 50ab1db5c0fd
child 57618 d762318438c3
clarified display;
src/Pure/PIDE/document.scala
src/Tools/jEdit/src/theories_dockable.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Wed Jul 23 14:50:20 2014 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Wed Jul 23 15:00:46 2014 +0200
     1.3 @@ -296,6 +296,9 @@
     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 +
    1.10      def + (entry: (Node.Name, Node)): Nodes =
    1.11      {
    1.12        val (name, node) = entry
     2.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Wed Jul 23 14:50:20 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Wed Jul 23 15:00:46 2014 +0200
     2.3 @@ -204,7 +204,7 @@
     2.4      val nodes_status1 =
     2.5        (nodes_status /: iterator)({ case (status, (name, node)) =>
     2.6            if (!name.is_theory || PIDE.resources.loaded_theories(name.theory)) status
     2.7 -          else if (node.is_empty) status - name
     2.8 +          else if (snapshot.version.nodes.is_maximal(name) && node.is_empty) status - name
     2.9            else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
    2.10  
    2.11      if (nodes_status != nodes_status1) {