src/Tools/jEdit/src/plugin.scala

--- a/src/Tools/jEdit/src/plugin.scala	Mon May 20 15:42:14 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Mon May 20 16:17:56 2013 +0200
@@ -196,7 +196,7 @@
               }
 
             case Session.Ready =>
-              PIDE.session.global_options.event(Session.Global_Options(PIDE.options.value))
+              PIDE.session.update_options(PIDE.options.value)
               PIDE.init_models(JEdit_Lib.jedit_buffers().toList)
               Swing_Thread.later { delay_load.invoke() }
 
@@ -270,7 +270,7 @@
           }
 
         case msg: PropertiesChanged =>
-          PIDE.session.global_options.event(Session.Global_Options(PIDE.options.value))
+          PIDE.session.update_options(PIDE.options.value)
 
         case _ =>
       }