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