tuned Commands_Changed: cover nodes as well;

--- a/src/Pure/System/session.scala	Wed Aug 31 15:41:22 2011 +0200
+++ b/src/Pure/System/session.scala	Wed Aug 31 17:22:49 2011 +0200
@@ -22,7 +22,7 @@
   case object Global_Settings
   case object Perspective
   case object Assignment
-  case class Commands_Changed(set: Set[Command])
+  case class Commands_Changed(nodes: Set[String], commands: Set[Command])
 
   sealed abstract class Phase
   case object Inactive extends Phase
@@ -63,7 +63,10 @@
   private val (_, command_change_buffer) =
     Simple_Thread.actor("command_change_buffer", daemon = true)
   {
-    var changed: Set[Command] = Set()
+    var changed_nodes: Set[String] = Set.empty
+    var changed_commands: Set[Command] = Set.empty
+    def changed: Boolean = !changed_nodes.isEmpty || !changed_commands.isEmpty
+
     var flush_time: Option[Long] = None
 
     def flush_timeout: Long =
@@ -74,8 +77,10 @@
 
     def flush()
     {
-      if (!changed.isEmpty) commands_changed.event(Session.Commands_Changed(changed))
-      changed = Set()
+      if (changed)
+        commands_changed.event(Session.Commands_Changed(changed_nodes, changed_commands))
+      changed_nodes = Set.empty
+      changed_commands = Set.empty
       flush_time = None
     }
 
@@ -91,7 +96,10 @@
     var finished = false
     while (!finished) {
       receiveWithin(flush_timeout) {
-        case command: Command => changed += command; invoke()
+        case command: Command =>
+          changed_nodes += command.node_name
+          changed_commands += command
+          invoke()
         case TIMEOUT => flush()
         case Stop => finished = true; reply(())
         case bad => System.err.println("command_change_buffer: ignoring bad message " + bad)

--- a/src/Tools/jEdit/src/document_view.scala	Wed Aug 31 15:41:22 2011 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Wed Aug 31 17:22:49 2011 +0200
@@ -442,27 +442,29 @@
   private val main_actor = actor {
     loop {
       react {
-        case Session.Commands_Changed(changed) =>
+        case changed: Session.Commands_Changed =>
           val buffer = model.buffer
           Isabelle.swing_buffer_lock(buffer) {
             val (updated, snapshot) = flush_snapshot()
             val visible = visible_range()
 
-            if (updated || changed.exists(snapshot.node.commands.contains))
+            if (updated ||
+                (changed.nodes.contains(model.node_name) &&
+                 changed.commands.exists(snapshot.node.commands.contains)))
               overview.repaint()
 
             if (updated) invalidate_range(visible)
             else {
               val visible_cmds =
                 snapshot.node.command_range(snapshot.revert(visible)).map(_._1)
-              if (visible_cmds.exists(changed)) {
+              if (visible_cmds.exists(changed.commands)) {
                 for {
                   line <- 0 until text_area.getVisibleLines
                   val start = text_area.getScreenLineStartOffset(line) if start >= 0
                   val end = text_area.getScreenLineEndOffset(line) if end >= 0
                   val range = proper_line_range(start, end)
                   val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
-                  if line_cmds.exists(changed)
+                  if line_cmds.exists(changed.commands)
                 } text_area.invalidateScreenLineRange(line, line)
               }
             }

--- a/src/Tools/jEdit/src/output_dockable.scala	Wed Aug 31 15:41:22 2011 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Wed Aug 31 17:22:49 2011 +0200
@@ -105,7 +105,7 @@
     loop {
       react {
         case Session.Global_Settings => handle_resize()
-        case Session.Commands_Changed(changed) => handle_update(Some(changed))
+        case changed: Session.Commands_Changed => handle_update(Some(changed.commands))
         case Session.Perspective => if (follow_caret && handle_perspective()) handle_update()
         case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
       }