# HG changeset patch
# User wenzelm
# Date 1452178209 -3600
# Node ID 9ace5f5bae697e4121cd7af248e2d2c31e946268
# Parent  c4d6066332408dc2303b34084d4fb26b8f145b32
more thorough GUI update;

diff -r c4d606633240 -r 9ace5f5bae69 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Thu Jan 07 13:42:43 2016 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Thu Jan 07 15:50:09 2016 +0100
@@ -256,7 +256,7 @@
     text_area.getGutter.addExtension(gutter_painter)
     text_area.addKeyListener(key_listener)
     text_area.addCaretListener(caret_listener)
-    text_area.addLeftOfScrollBar(overview)
+    text_area.addLeftOfScrollBar(overview); text_area.revalidate(); text_area.repaint()
     Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)).
       foreach(text_area.addStructureMatcher(_))
     session.raw_edits += main
@@ -271,7 +271,7 @@
     session.commands_changed -= main
     Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)).
       foreach(text_area.removeStructureMatcher(_))
-    text_area.removeLeftOfScrollBar(overview); overview.revoke()
+    overview.revoke(); text_area.removeLeftOfScrollBar(overview)
     text_area.removeCaretListener(caret_listener); delay_caret_update.revoke()
     text_area.removeKeyListener(key_listener)
     text_area.getGutter.removeExtension(gutter_painter)
diff -r c4d606633240 -r 9ace5f5bae69 src/Tools/jEdit/src/text_overview.scala
--- a/src/Tools/jEdit/src/text_overview.scala	Thu Jan 07 13:42:43 2016 +0100
+++ b/src/Tools/jEdit/src/text_overview.scala	Thu Jan 07 15:50:09 2016 +0100
@@ -82,7 +82,13 @@
         val rendering = doc_view.get_rendering()
         val overview = get_overview()
 
-        if (!rendering.snapshot.is_outdated && overview == current_overview) {
+        if (rendering.snapshot.is_outdated || overview != current_overview) {
+          invoke()
+
+          gfx.setColor(rendering.outdated_color)
+          gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
+        }
+        else {
           gfx.setColor(getBackground)
           gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
           for ((color, h, h1) <- current_colors) {
@@ -90,10 +96,6 @@
             gfx.fillRect(0, h, getWidth, h1 - h)
           }
         }
-        else {
-          gfx.setColor(rendering.outdated_color)
-          gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
-        }
       }
     }
   }