src/Tools/jEdit/src/document_view.scala

         val start = text_area.getScreenLineStartOffset(i)
         val stop = text_area.getScreenLineEndOffset(i)
         if start >= 0 && stop >= 0
       }
       yield Text.Range(start, stop))
+  }
+
+  private def update_perspective = new TextAreaExtension
+  {
+    override def paintScreenLineRange(gfx: Graphics2D,
+      first_line: Int, last_line: Int, physical_lines: Array[Int],
+      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
+    {
+      model.update_perspective()
+    }
   }
 
 
   /* snapshot */
 

     }
     override def caretUpdate(e: CaretEvent) { delay() }
   }
 
 
-  /* scrolling */
-
-  private val scroll_listener = new ScrollListener
-  {
-    def scrolledVertically(arg: TextArea) { model.update_perspective() }
-    def scrolledHorizontally(arg: TextArea) { }
-  }
-
-
   /* overview of command status left of scrollbar */
 
   private val overview = new JPanel(new BorderLayout)
   {
     private val WIDTH = 10

   /* activation */
 
   private def activate()
   {
     val painter = text_area.getPainter
+    painter.addExtension(TextAreaPainter.LOWEST_LAYER, update_perspective)
     painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, tooltip_painter)
     text_area_painter.activate()
     text_area.getGutter.addExtension(gutter_painter)
     text_area.addFocusListener(focus_listener)
     text_area.getView.addWindowListener(window_listener)
     painter.addMouseMotionListener(mouse_motion_listener)
     text_area.addCaretListener(caret_listener)
-    text_area.addScrollListener(scroll_listener)
     text_area.addLeftOfScrollBar(overview)
     session.commands_changed += main_actor
     session.global_settings += main_actor
   }
 

     session.global_settings -= main_actor
     text_area.removeFocusListener(focus_listener)
     text_area.getView.removeWindowListener(window_listener)
     painter.removeMouseMotionListener(mouse_motion_listener)
     text_area.removeCaretListener(caret_listener)
-    text_area.removeScrollListener(scroll_listener)
     text_area.removeLeftOfScrollBar(overview)
     text_area.getGutter.removeExtension(gutter_painter)
     text_area_painter.deactivate()
     painter.removeExtension(tooltip_painter)
+    painter.removeExtension(update_perspective)
     exit_popup()
   }
 }