# HG changeset patch
# User wenzelm
# Date 1429099288 -7200
# Node ID b079ee0e766cb15797a0b55b67840b464b84095a
# Parent  38a64cc17403b825b1bee7bdd89acba47bc28e97
obsolete (see also 94b2690ad494);

diff -r 38a64cc17403 -r b079ee0e766c src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Wed Apr 15 13:55:01 2015 +0200
+++ b/src/Pure/PIDE/session.scala	Wed Apr 15 14:01:28 2015 +0200
@@ -624,11 +624,6 @@
   def update_options(options: Options)
   { manager.send_wait(Update_Options(options)) }
 
-  def init_options(options: Options)
-  {
-    update_options(options)
-  }
-
   def dialog_result(id: Document_ID.Generic, serial: Long, result: String)
   { manager.send(Session.Dialog_Result(id, serial, result)) }
 
diff -r 38a64cc17403 -r b079ee0e766c src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Wed Apr 15 13:55:01 2015 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Apr 15 14:01:28 2015 +0200
@@ -261,7 +261,7 @@
         }
 
       case Session.Ready =>
-        PIDE.session.init_options(PIDE.options.value)
+        PIDE.session.update_options(PIDE.options.value)
         PIDE.init_models()
 
         if (!Isabelle.continuous_checking) {