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