changeset 43396 | 548a68eafaea |
parent 43393 | f4141da52e92 |
child 43398 | c3e2a361b418 |
--- 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)