# HG changeset patch
# User wenzelm
# Date 1283269785 -7200
# Node ID 9ec5f6010d6e2ce7e34d79f7b65ce136024a9f5f
# Parent  0998a635684a7c4c56cce31b73dc6629db55fad0
Document_View: repaint overview for any command change of this node (again);

diff -r 0998a635684a -r 9ec5f6010d6e src/Tools/jEdit/src/jedit/document_view.scala
--- 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()
             }
           }