--- 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)
--- 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)
- }
}
}
}