--- 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) {