src/Tools/jEdit/src/session_dockable.scala
changeset 44672 07dad1433cd7
parent 44641 101c117494cd
child 44734 7313e2db3d39
     1.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Fri Sep 02 16:58:00 2011 -0700
     1.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Sat Sep 03 12:31:27 2011 +0200
     1.3 @@ -80,23 +80,21 @@
     1.4      Swing_Thread.now {
     1.5        // FIXME correlation to changed_nodes!?
     1.6        val state = Isabelle.session.current_state()
     1.7 -      state.recent_stable.map(change => change.version.get_finished) match {
     1.8 -        case None =>
     1.9 -        case Some(version) =>
    1.10 -          var nodes_status1 = nodes_status
    1.11 -          for {
    1.12 -            name <- changed_nodes
    1.13 -            node <- version.nodes.get(name)
    1.14 -            val status = Isar_Document.node_status(state, version, node)
    1.15 -          } nodes_status1 += (name -> status.toString)
    1.16 +      val version = state.recent_stable.version.get_finished
    1.17  
    1.18 -          if (nodes_status != nodes_status1) {
    1.19 -            nodes_status = nodes_status1
    1.20 -            val order =
    1.21 -              Library.sort_wrt((name: Document.Node.Name) => name.theory,
    1.22 -                nodes_status.keySet.toList)
    1.23 -            status.listData = order.map(name => name.theory + " " + nodes_status(name))
    1.24 -          }
    1.25 +      var nodes_status1 = nodes_status
    1.26 +      for {
    1.27 +        name <- changed_nodes
    1.28 +        node <- version.nodes.get(name)
    1.29 +        val status = Isar_Document.node_status(state, version, node)
    1.30 +      } nodes_status1 += (name -> status.toString)
    1.31 +
    1.32 +      if (nodes_status != nodes_status1) {
    1.33 +        nodes_status = nodes_status1
    1.34 +        val order =
    1.35 +          Library.sort_wrt((name: Document.Node.Name) => name.theory,
    1.36 +            nodes_status.keySet.toList)
    1.37 +        status.listData = order.map(name => name.theory + " " + nodes_status(name))
    1.38        }
    1.39      }
    1.40    }