# HG changeset patch
# User wenzelm
# Date 1460659664 -7200
# Node ID 4be23c432491dde28494334d3cfe0fa8e89f8727
# Parent  61b32a6d87e9462dbfb50ff7e6372ad3266f8a1d
tuned;

diff -r 61b32a6d87e9 -r 4be23c432491 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Thu Apr 14 17:03:55 2016 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Thu Apr 14 20:47:44 2016 +0200
@@ -194,7 +194,7 @@
 
   /* text status overview left of scrollbar */
 
-  private val overview = new Text_Overview(this)
+  private val text_overview = new Text_Overview(this)
 
 
   /* main */
@@ -202,7 +202,7 @@
   private val main =
     Session.Consumer[Any](getClass.getName) {
       case _: Session.Raw_Edits =>
-        overview.invoke()
+        text_overview.invoke()
 
       case changed: Session.Commands_Changed =>
         val buffer = model.buffer
@@ -217,7 +217,7 @@
               if (changed.assignment || load_changed ||
                   (changed.nodes.contains(model.node_name) &&
                    changed.commands.exists(snapshot.node.commands.contains)))
-                overview.invoke()
+                text_overview.invoke()
 
               val visible_lines = text_area.getVisibleLines
               if (visible_lines > 0) {
@@ -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.revalidate(); text_area.repaint()
+    text_area.addLeftOfScrollBar(text_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(_))
-    overview.revoke(); text_area.removeLeftOfScrollBar(overview)
+    text_overview.revoke(); text_area.removeLeftOfScrollBar(text_overview)
     text_area.removeCaretListener(caret_listener); delay_caret_update.revoke()
     text_area.removeKeyListener(key_listener)
     text_area.getGutter.removeExtension(gutter_painter)