361 painter.addMouseMotionListener(mouse_motion_listener) |
361 painter.addMouseMotionListener(mouse_motion_listener) |
362 text_area.addCaretListener(caret_listener) |
362 text_area.addCaretListener(caret_listener) |
363 text_area.addLeftOfScrollBar(overview) |
363 text_area.addLeftOfScrollBar(overview) |
364 session.raw_edits += main_actor |
364 session.raw_edits += main_actor |
365 session.commands_changed += main_actor |
365 session.commands_changed += main_actor |
366 session.global_settings += main_actor |
|
367 } |
366 } |
368 |
367 |
369 private def deactivate() |
368 private def deactivate() |
370 { |
369 { |
371 val painter = text_area.getPainter |
370 val painter = text_area.getPainter |
372 session.raw_edits -= main_actor |
371 session.raw_edits -= main_actor |
373 session.commands_changed -= main_actor |
372 session.commands_changed -= main_actor |
374 session.global_settings -= main_actor |
|
375 text_area.removeFocusListener(focus_listener) |
373 text_area.removeFocusListener(focus_listener) |
376 text_area.getView.removeWindowListener(window_listener) |
374 text_area.getView.removeWindowListener(window_listener) |
377 painter.removeMouseMotionListener(mouse_motion_listener) |
375 painter.removeMouseMotionListener(mouse_motion_listener) |
378 painter.removeMouseListener(mouse_listener) |
376 painter.removeMouseListener(mouse_listener) |
379 text_area.removeCaretListener(caret_listener); delay_caret_update.revoke() |
377 text_area.removeCaretListener(caret_listener); delay_caret_update.revoke() |