# HG changeset patch
# User wenzelm
# Date 1453405834 -3600
# Node ID 6eeaaefcea560b763923bb84fb42a3cb22cf4b8d
# Parent  9f7293af6fb8dee870c60608f7bae808018e42b8
clarified errors: more explicit treatment of uninitialized state;

diff -r 9f7293af6fb8 -r 6eeaaefcea56 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Wed Jan 20 23:19:52 2016 +0100
+++ b/src/Pure/System/options.scala	Thu Jan 21 20:50:34 2016 +0100
@@ -387,48 +387,52 @@
 
 class Options_Variable
 {
-  private var options = Options.empty
+  private var options: Option[Options] = None
+
+  def store(new_options: Options): Unit = synchronized { options = Some(new_options) }
 
-  def value: Options = synchronized { options }
-  def update(new_options: Options): Unit = synchronized { options = new_options }
+  def value: Options = synchronized {
+    options match {
+      case Some(opts) => opts
+      case None => error("Uninitialized Isabelle system options")
+    }
+  }
 
-  def + (name: String, x: String): Unit = synchronized { options = options + (name, x) }
+  private def upd(f: Options => Options): Unit = synchronized { options = Some(f(value)) }
+
+  def + (name: String, x: String): Unit = upd(opts => opts + (name, x))
 
   class Bool_Access
   {
-    def apply(name: String): Boolean = synchronized { options.bool(name) }
-    def update(name: String, x: Boolean): Unit =
-      synchronized { options = options.bool.update(name, x) }
+    def apply(name: String): Boolean = value.bool(name)
+    def update(name: String, x: Boolean): Unit = upd(opts => opts.bool.update(name, x))
   }
   val bool = new Bool_Access
 
   class Int_Access
   {
-    def apply(name: String): Int = synchronized { options.int(name) }
-    def update(name: String, x: Int): Unit =
-      synchronized { options = options.int.update(name, x) }
+    def apply(name: String): Int = value.int(name)
+    def update(name: String, x: Int): Unit = upd(opts => opts.int.update(name, x))
   }
   val int = new Int_Access
 
   class Real_Access
   {
-    def apply(name: String): Double = synchronized { options.real(name) }
-    def update(name: String, x: Double): Unit =
-      synchronized { options = options.real.update(name, x) }
+    def apply(name: String): Double = value.real(name)
+    def update(name: String, x: Double): Unit = upd(opts => opts.real.update(name, x))
   }
   val real = new Real_Access
 
   class String_Access
   {
-    def apply(name: String): String = synchronized { options.string(name) }
-    def update(name: String, x: String): Unit =
-      synchronized { options = options.string.update(name, x) }
+    def apply(name: String): String = value.string(name)
+    def update(name: String, x: String): Unit = upd(opts => opts.string.update(name, x))
   }
   val string = new String_Access
 
   class Seconds_Access
   {
-    def apply(name: String): Time = synchronized { options.seconds(name) }
+    def apply(name: String): Time = value.seconds(name)
   }
   val seconds = new Seconds_Access
 }
diff -r 9f7293af6fb8 -r 6eeaaefcea56 src/Tools/jEdit/src/jedit_options.scala
--- a/src/Tools/jEdit/src/jedit_options.scala	Wed Jan 20 23:19:52 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_options.scala	Thu Jan 21 20:50:34 2016 +0100
@@ -96,7 +96,7 @@
             val title = opt_title
             def load = text = value.check_name(opt_name).value
             def save =
-              try { update(value + (opt_name, text)) }
+              try { store(value + (opt_name, text)) }
               catch {
                 case ERROR(msg) =>
                   GUI.error_dialog(this.peer, "Failed to update options",
diff -r 9f7293af6fb8 -r 6eeaaefcea56 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Wed Jan 20 23:19:52 2016 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Jan 21 20:50:34 2016 +0100
@@ -391,7 +391,7 @@
       Debug.DISABLE_SEARCH_DIALOG_POOL = true
 
       PIDE.plugin = this
-      PIDE.options.update(Options.init())
+      PIDE.options.store(Options.init())
       PIDE.completion_history.load()
       PIDE.spell_checker.update(PIDE.options.value)