src/Tools/jEdit/src/session_dockable.scala
changeset 46681 c083a3f621c0
parent 45709 87017fcbad83
child 46688 134982ee4ecb
     1.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Sun Feb 26 17:15:33 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Sun Feb 26 17:44:09 2012 +0100
     1.3 @@ -146,14 +146,13 @@
     1.4    {
     1.5      Swing_Thread.now {
     1.6        val snapshot = Isabelle.session.snapshot()
     1.7 -      val nodes = restriction getOrElse snapshot.version.nodes.keySet
     1.8 +      val names = restriction getOrElse snapshot.version.nodes.keySet
     1.9  
    1.10 -      var nodes_status1 = nodes_status
    1.11 -      for {
    1.12 -        name <- nodes
    1.13 -        node <- snapshot.version.nodes.get(name)
    1.14 -        val status = Protocol.node_status(snapshot.state, snapshot.version, node)
    1.15 -      } nodes_status1 += (name -> status)
    1.16 +      val nodes_status1 =
    1.17 +        (nodes_status /: names)((status, name) => {
    1.18 +          val node = snapshot.version.nodes(name)
    1.19 +          status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node))
    1.20 +        })
    1.21  
    1.22        if (nodes_status != nodes_status1) {
    1.23          nodes_status = nodes_status1