Document_View: repaint overview for any command change of this node (again);

--- a/src/Tools/jEdit/src/jedit/document_view.scala	Tue Aug 31 17:40:32 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Tue Aug 31 17:49:45 2010 +0200
@@ -125,6 +125,9 @@
           Isabelle.swing_buffer_lock(buffer) {
             val snapshot = model.snapshot()
 
+            if (changed.exists(snapshot.node.commands.contains))
+              overview.repaint()
+
             val visible_range = screen_lines_range()
             val visible_cmds = snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
             if (visible_cmds.exists(changed)) {
@@ -136,12 +139,10 @@
                 val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
                 if line_cmds.exists(changed)
               } text_area.invalidateScreenLineRange(line, line)
+
               // FIXME danger of deadlock!?
               // FIXME potentially slow!?
               model.buffer.propertiesChanged()
-
-              // FIXME really paint here!?
-              overview.repaint()
             }
           }