no longer react on global_settings (cf. 34ac36642a31);
--- a/src/Tools/jEdit/src/document_view.scala Fri Sep 14 20:49:54 2012 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Fri Sep 14 21:15:59 2012 +0200
@@ -363,7 +363,6 @@
text_area.addLeftOfScrollBar(overview)
session.raw_edits += main_actor
session.commands_changed += main_actor
- session.global_settings += main_actor
}
private def deactivate()
@@ -371,7 +370,6 @@
val painter = text_area.getPainter
session.raw_edits -= main_actor
session.commands_changed -= main_actor
- session.global_settings -= main_actor
text_area.removeFocusListener(focus_listener)
text_area.getView.removeWindowListener(window_listener)
painter.removeMouseMotionListener(mouse_motion_listener)