src/Tools/jEdit/src/document_view.scala
changeset 43387 a59ae768249e
parent 43381 806878ae2219
child 43390 7ee98a3802af
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Tue Jun 14 14:33:46 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Tue Jun 14 14:55:22 2011 +0200
     1.3 @@ -406,7 +406,7 @@
     1.4    private def activate()
     1.5    {
     1.6      val painter = text_area.getPainter
     1.7 -    painter.addExtension(TextAreaPainter.TEXT_LAYER, tooltip_painter)
     1.8 +    painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, tooltip_painter)
     1.9      text_area_painter.activate()
    1.10      text_area.getGutter.addExtension(gutter_painter)
    1.11      text_area.addFocusListener(focus_listener)