equal
deleted
inserted
replaced
346 } |
346 } |
347 |
347 |
348 def deactivate() |
348 def deactivate() |
349 { |
349 { |
350 val painter = text_area.getPainter |
350 val painter = text_area.getPainter |
|
351 painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter) |
351 painter.removeExtension(reset_state) |
352 painter.removeExtension(reset_state) |
352 painter.removeExtension(caret_painter) |
353 painter.removeExtension(caret_painter) |
353 painter.removeExtension(after_caret_painter2) |
354 painter.removeExtension(after_caret_painter2) |
354 painter.removeExtension(before_caret_painter2) |
355 painter.removeExtension(before_caret_painter2) |
355 painter.removeExtension(after_caret_painter1) |
356 painter.removeExtension(after_caret_painter1) |