clarified display;
authorwenzelm
Wed Jul 23 15:32:05 2014 +0200 (2014-07-23)
changeset 57619dcd69422b953
parent 57618 d762318438c3
child 57620 c30ab960875e
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 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      {
     2.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Wed Jul 23 15:11:42 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Wed Jul 23 15:32:05 2014 +0200
     2.3 @@ -195,23 +195,25 @@
     2.4      GUI_Thread.require {}
     2.5  
     2.6      val snapshot = PIDE.session.snapshot()
     2.7 +    val nodes = snapshot.version.nodes
     2.8  
     2.9      val iterator =
    2.10        restriction match {
    2.11 -        case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
    2.12 -        case None => snapshot.version.nodes.iterator
    2.13 +        case Some(names) => names.iterator.map(name => (name, nodes(name)))
    2.14 +        case None => nodes.iterator
    2.15        }
    2.16      val nodes_status1 =
    2.17        (nodes_status /: iterator)({ case (status, (name, node)) =>
    2.18 -          if (!name.is_theory || PIDE.resources.loaded_theories(name.theory)) status
    2.19 -          else if (snapshot.version.nodes.is_maximal(name) && node.is_empty) status - name
    2.20 +          if (!name.is_theory || PIDE.resources.loaded_theories(name.theory) || node.is_empty)
    2.21 +            status
    2.22            else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
    2.23  
    2.24 -    if (nodes_status != nodes_status1) {
    2.25 -      nodes_status = nodes_status1
    2.26 -      status.listData =
    2.27 -        snapshot.version.nodes.topological_order.filter(
    2.28 -          (name: Document.Node.Name) => nodes_status.isDefinedAt(name))
    2.29 +    val nodes_status2 =
    2.30 +      nodes_status1 -- nodes_status1.keysIterator.filter(nodes.is_hidden(_))
    2.31 +
    2.32 +    if (nodes_status != nodes_status2) {
    2.33 +      nodes_status = nodes_status2
    2.34 +      status.listData = nodes.topological_order.filter(nodes_status.isDefinedAt(_))
    2.35      }
    2.36    }
    2.37