author | wenzelm |
Wed, 15 Jun 2011 15:42:54 +0200 | |
changeset 43396 | 548a68eafaea |
parent 43395 | 85e468a8045a |
child 43397 | dba359c0ae3b |
--- 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)