recovered tooltip Entity content (odd effect of layer change!? cf. 806878ae2219);
authorwenzelm
Tue, 14 Jun 2011 14:55:22 +0200
changeset 43387 a59ae768249e
parent 43386 4e78dd88c64f
child 43388 34492601c0e0
recovered tooltip Entity content (odd effect of layer change!? cf. 806878ae2219);
src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Tue Jun 14 14:33:46 2011 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Tue Jun 14 14:55:22 2011 +0200
@@ -406,7 +406,7 @@
   private def activate()
   {
     val painter = text_area.getPainter
-    painter.addExtension(TextAreaPainter.TEXT_LAYER, tooltip_painter)
+    painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, tooltip_painter)
     text_area_painter.activate()
     text_area.getGutter.addExtension(gutter_painter)
     text_area.addFocusListener(focus_listener)