# HG changeset patch
# User wenzelm
# Date 1308056122 -7200
# Node ID a59ae768249e1e85c1a6133d9b7fb5c977aadc43
# Parent  4e78dd88c64fd7cd5d8d7c221aa501fa6d11a7d2
recovered tooltip Entity content (odd effect of layer change!? cf. 806878ae2219);

diff -r 4e78dd88c64f -r a59ae768249e 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)