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)