# HG changeset patch # User wenzelm # Date 1489517213 -3600 # Node ID 4fa82bbb394e28fbe24d2edc01091b9c3ce8a0bf # Parent fe6d2cd61009d70ac5e0babcfcf5568a82ad8187 afford early initialization of JEdit_Options, but it may lead to messy exception trace for malformed etc/preferences (see also 6eeaaefcea56); tuned signature; diff -r fe6d2cd61009 -r 4fa82bbb394e src/Pure/System/options.scala --- a/src/Pure/System/options.scala Tue Mar 14 19:40:39 2017 +0100 +++ b/src/Pure/System/options.scala Tue Mar 14 19:46:53 2017 +0100 @@ -415,22 +415,14 @@ } -class Options_Variable +class Options_Variable(init_options: Options) { - private var options: Option[Options] = None - - def store(new_options: Options): Unit = synchronized { options = Some(new_options) } + private var options = init_options - def value: Options = synchronized { - options match { - case Some(opts) => opts - case None => error("Uninitialized Isabelle system options") - } - } + def value: Options = synchronized { options } - private def upd(f: Options => Options): Unit = synchronized { options = Some(f(value)) } - - def + (name: String, x: String): Unit = upd(opts => opts + (name, x)) + private def upd(f: Options => Options): Unit = synchronized { options = f(options) } + def += (name: String, x: String): Unit = upd(opts => opts + (name, x)) class Bool_Access { diff -r fe6d2cd61009 -r 4fa82bbb394e src/Tools/jEdit/src/jedit_options.scala --- a/src/Tools/jEdit/src/jedit_options.scala Tue Mar 14 19:40:39 2017 +0100 +++ b/src/Tools/jEdit/src/jedit_options.scala Tue Mar 14 19:46:53 2017 +0100 @@ -49,7 +49,7 @@ } } -class JEdit_Options extends Options_Variable +class JEdit_Options(init_options: Options) extends Options_Variable(init_options) { def color_value(s: String): Color = Color_Value(string(s)) @@ -96,7 +96,7 @@ val title = opt_title def load = text = value.check_name(opt_name).value def save = - try { store(value + (opt_name, text)) } + try { JEdit_Options.this += (opt_name, text) } catch { case ERROR(msg) => GUI.error_dialog(this.peer, "Failed to update options", diff -r fe6d2cd61009 -r 4fa82bbb394e src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Tue Mar 14 19:40:39 2017 +0100 +++ b/src/Tools/jEdit/src/plugin.scala Tue Mar 14 19:46:53 2017 +0100 @@ -29,7 +29,7 @@ { /* plugin instance */ - val options = new JEdit_Options + lazy val options = new JEdit_Options(Options.init()) val completion_history = new Completion.History_Variable val spell_checker = new Spell_Checker_Variable @@ -380,7 +380,6 @@ Debug.DISABLE_SEARCH_DIALOG_POOL = true PIDE.plugin = this - PIDE.options.store(Options.init()) PIDE.completion_history.load() PIDE.spell_checker.update(PIDE.options.value)