obsolete (see also 94b2690ad494);
authorwenzelm
Wed, 15 Apr 2015 14:01:28 +0200
changeset 60075 b079ee0e766c
parent 60074 38a64cc17403
child 60076 e24f59cba23c
obsolete (see also 94b2690ad494);
src/Pure/PIDE/session.scala
src/Tools/jEdit/src/plugin.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)) }
 
--- 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) {