1.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Tue Sep 20 15:07:30 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Tue Sep 20 15:23:17 2011 +0200
     1.3 @@ -139,15 +139,15 @@
     1.4    }
     1.5    status.renderer = new Node_Renderer
     1.6  
     1.7 -  private def handle_changed(changed_nodes: Set[Document.Node.Name])
     1.8 +  private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
     1.9    {
    1.10      Swing_Thread.now {
    1.11 -      // FIXME correlation to changed_nodes!?
    1.12        val snapshot = Isabelle.session.snapshot()
    1.13 +      val nodes = restriction getOrElse snapshot.version.nodes.keySet
    1.14  
    1.15        var nodes_status1 = nodes_status
    1.16        for {
    1.17 -        name <- changed_nodes
    1.18 +        name <- nodes
    1.19          node <- snapshot.version.nodes.get(name)
    1.20          val status = Isar_Document.node_status(snapshot.state, snapshot.version, node)
    1.21        } nodes_status1 += (name -> status)
    1.22 @@ -179,7 +179,7 @@
    1.23          case phase: Session.Phase =>
    1.24            Swing_Thread.now { session_phase.text = " " + phase.toString + " " }
    1.25  
    1.26 -        case changed: Session.Commands_Changed => handle_changed(changed.nodes)
    1.27 +        case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))
    1.28  
    1.29          case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
    1.30        }
    1.31 @@ -197,4 +197,6 @@
    1.32      Isabelle.session.phase_changed -= main_actor
    1.33      Isabelle.session.commands_changed -= main_actor
    1.34    }
    1.35 +
    1.36 +  handle_update()
    1.37  }