recovered orig_text_painter from f4141da52e92;
authorwenzelm
Wed Jun 15 15:42:54 2011 +0200 (2011-06-15)
changeset 43396548a68eafaea
parent 43395 85e468a8045a
child 43397 dba359c0ae3b
recovered orig_text_painter from f4141da52e92;
src/Tools/jEdit/src/text_area_painter.scala
     1.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Wed Jun 15 15:08:22 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Wed Jun 15 15:42:54 2011 +0200
     1.3 @@ -348,6 +348,7 @@
     1.4    def deactivate()
     1.5    {
     1.6      val painter = text_area.getPainter
     1.7 +    painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
     1.8      painter.removeExtension(reset_state)
     1.9      painter.removeExtension(caret_painter)
    1.10      painter.removeExtension(after_caret_painter2)