# HG changeset patch
# User wenzelm
# Date 1316524997 -7200
# Node ID 436ea69d5d379a7d840b4b67bf4c54e522d11f8f
# Parent  8a4db903039fdd16fba0ebd1e5107db0e244194b
more careful treatment of initial update, similar to output panel;

diff -r 8a4db903039f -r 436ea69d5d37 src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Tue Sep 20 15:07:30 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Tue Sep 20 15:23:17 2011 +0200
@@ -139,15 +139,15 @@
   }
   status.renderer = new Node_Renderer
 
-  private def handle_changed(changed_nodes: Set[Document.Node.Name])
+  private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
   {
     Swing_Thread.now {
-      // FIXME correlation to changed_nodes!?
       val snapshot = Isabelle.session.snapshot()
+      val nodes = restriction getOrElse snapshot.version.nodes.keySet
 
       var nodes_status1 = nodes_status
       for {
-        name <- changed_nodes
+        name <- nodes
         node <- snapshot.version.nodes.get(name)
         val status = Isar_Document.node_status(snapshot.state, snapshot.version, node)
       } nodes_status1 += (name -> status)
@@ -179,7 +179,7 @@
         case phase: Session.Phase =>
           Swing_Thread.now { session_phase.text = " " + phase.toString + " " }
 
-        case changed: Session.Commands_Changed => handle_changed(changed.nodes)
+        case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))
 
         case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
       }
@@ -197,4 +197,6 @@
     Isabelle.session.phase_changed -= main_actor
     Isabelle.session.commands_changed -= main_actor
   }
+
+  handle_update()
 }