# HG changeset patch
# User wenzelm
# Date 1308145374 -7200
# Node ID 548a68eafaea2fb13d28acf487d270b543f240de
# Parent  85e468a8045a7f21bbe06f9047e2a2735f55c635
recovered orig_text_painter from f4141da52e92;

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)