src/Tools/jEdit/src/document_view.scala
changeset 62985 4be23c432491
parent 62092 9ace5f5bae69
child 62986 9d2fae6b31cc
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Thu Apr 14 17:03:55 2016 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Thu Apr 14 20:47:44 2016 +0200
     1.3 @@ -194,7 +194,7 @@
     1.4  
     1.5    /* text status overview left of scrollbar */
     1.6  
     1.7 -  private val overview = new Text_Overview(this)
     1.8 +  private val text_overview = new Text_Overview(this)
     1.9  
    1.10  
    1.11    /* main */
    1.12 @@ -202,7 +202,7 @@
    1.13    private val main =
    1.14      Session.Consumer[Any](getClass.getName) {
    1.15        case _: Session.Raw_Edits =>
    1.16 -        overview.invoke()
    1.17 +        text_overview.invoke()
    1.18  
    1.19        case changed: Session.Commands_Changed =>
    1.20          val buffer = model.buffer
    1.21 @@ -217,7 +217,7 @@
    1.22                if (changed.assignment || load_changed ||
    1.23                    (changed.nodes.contains(model.node_name) &&
    1.24                     changed.commands.exists(snapshot.node.commands.contains)))
    1.25 -                overview.invoke()
    1.26 +                text_overview.invoke()
    1.27  
    1.28                val visible_lines = text_area.getVisibleLines
    1.29                if (visible_lines > 0) {
    1.30 @@ -256,7 +256,7 @@
    1.31      text_area.getGutter.addExtension(gutter_painter)
    1.32      text_area.addKeyListener(key_listener)
    1.33      text_area.addCaretListener(caret_listener)
    1.34 -    text_area.addLeftOfScrollBar(overview); text_area.revalidate(); text_area.repaint()
    1.35 +    text_area.addLeftOfScrollBar(text_overview); text_area.revalidate(); text_area.repaint()
    1.36      Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)).
    1.37        foreach(text_area.addStructureMatcher(_))
    1.38      session.raw_edits += main
    1.39 @@ -271,7 +271,7 @@
    1.40      session.commands_changed -= main
    1.41      Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)).
    1.42        foreach(text_area.removeStructureMatcher(_))
    1.43 -    overview.revoke(); text_area.removeLeftOfScrollBar(overview)
    1.44 +    text_overview.revoke(); text_area.removeLeftOfScrollBar(text_overview)
    1.45      text_area.removeCaretListener(caret_listener); delay_caret_update.revoke()
    1.46      text_area.removeKeyListener(key_listener)
    1.47      text_area.getGutter.removeExtension(gutter_painter)