author | wenzelm |
Mon, 31 Mar 2014 20:07:59 +0200 | |
changeset 56340 | af8cb60b55eb |
parent 56339 | ce37fcb30cf2 |
child 56341 | bfd13102eb54 |
--- a/src/Tools/jEdit/src/rich_text_area.scala Mon Mar 31 18:28:35 2014 +0200 +++ b/src/Tools/jEdit/src/rich_text_area.scala Mon Mar 31 20:07:59 2014 +0200 @@ -590,6 +590,7 @@ def deactivate() { + active_reset() val painter = text_area.getPainter view.removeWindowListener(window_listener) text_area.removeFocusListener(focus_listener)