src/Tools/jEdit/src/document_view.scala
changeset 44436 546adfa8a6fc
parent 44379 1079ab6b342b
child 44437 bebe15799192
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Tue Aug 23 21:19:24 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Wed Aug 24 13:03:39 2011 +0200
     1.3 @@ -25,7 +25,8 @@
     1.4  import org.gjt.sp.jedit.{jEdit, OperatingSystem, Debug}
     1.5  import org.gjt.sp.jedit.gui.RolloverButton
     1.6  import org.gjt.sp.jedit.options.GutterOptionPane
     1.7 -import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
     1.8 +import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter,
     1.9 +  ScrollListener}
    1.10  import org.gjt.sp.jedit.syntax.{SyntaxStyle}
    1.11  
    1.12  
    1.13 @@ -354,6 +355,15 @@
    1.14    }
    1.15  
    1.16  
    1.17 +  /* scrolling */
    1.18 +
    1.19 +  private val scroll_listener = new ScrollListener
    1.20 +  {
    1.21 +    def scrolledVertically(arg: TextArea) { model.update_perspective() }
    1.22 +    def scrolledHorizontally(arg: TextArea) { }
    1.23 +  }
    1.24 +
    1.25 +
    1.26    /* overview of command status left of scrollbar */
    1.27  
    1.28    private val overview = new JPanel(new BorderLayout)
    1.29 @@ -474,6 +484,7 @@
    1.30      text_area.getView.addWindowListener(window_listener)
    1.31      painter.addMouseMotionListener(mouse_motion_listener)
    1.32      text_area.addCaretListener(caret_listener)
    1.33 +    text_area.addScrollListener(scroll_listener)
    1.34      text_area.addLeftOfScrollBar(overview)
    1.35      session.commands_changed += main_actor
    1.36      session.global_settings += main_actor
    1.37 @@ -488,6 +499,7 @@
    1.38      text_area.getView.removeWindowListener(window_listener)
    1.39      painter.removeMouseMotionListener(mouse_motion_listener)
    1.40      text_area.removeCaretListener(caret_listener)
    1.41 +    text_area.removeScrollListener(scroll_listener)
    1.42      text_area.removeLeftOfScrollBar(overview)
    1.43      text_area.getGutter.removeExtension(gutter_painter)
    1.44      text_area_painter.deactivate()