diff -r 85e468a8045a -r 548a68eafaea src/Tools/jEdit/src/text_area_painter.scala --- a/src/Tools/jEdit/src/text_area_painter.scala Wed Jun 15 15:08:22 2011 +0200 +++ b/src/Tools/jEdit/src/text_area_painter.scala Wed Jun 15 15:42:54 2011 +0200 @@ -348,6 +348,7 @@ def deactivate() { val painter = text_area.getPainter + painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter) painter.removeExtension(reset_state) painter.removeExtension(caret_painter) painter.removeExtension(after_caret_painter2)