--- 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)