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