--- a/src/Pure/System/options.scala Sat Aug 13 16:12:22 2022 +0200
+++ b/src/Pure/System/options.scala Sat Aug 13 16:24:14 2022 +0200
@@ -15,12 +15,12 @@
/* access */
- trait Access[A] {
+ abstract class Access[A](val options: Options) {
def apply(name: String): A
def update(name: String, x: A): Options
}
- trait Access_Variable[A] {
+ abstract class Access_Variable[A](val options: Options_Variable) {
def apply(name: String): A
def update(name: String, x: A): Unit
}
@@ -265,29 +265,29 @@
/* internal lookup and update */
- class Bool_Access extends Options.Access[Boolean] {
- def apply(name: String): Boolean = get(name, Options.Bool, Value.Boolean.unapply)
- def update(name: String, x: Boolean): Options = put(name, Options.Bool, Value.Boolean(x))
- }
- val bool = new Bool_Access
+ val bool: Options.Access[Boolean] =
+ new Options.Access[Boolean](this) {
+ def apply(name: String): Boolean = get(name, Options.Bool, Value.Boolean.unapply)
+ def update(name: String, x: Boolean): Options = put(name, Options.Bool, Value.Boolean(x))
+ }
- class Int_Access extends Options.Access[Int] {
- def apply(name: String): Int = get(name, Options.Int, Value.Int.unapply)
- def update(name: String, x: Int): Options = put(name, Options.Int, Value.Int(x))
- }
- val int = new Int_Access
+ val int: Options.Access[Int] =
+ new Options.Access[Int](this) {
+ def apply(name: String): Int = get(name, Options.Int, Value.Int.unapply)
+ def update(name: String, x: Int): Options = put(name, Options.Int, Value.Int(x))
+ }
- class Real_Access extends Options.Access[Double] {
- def apply(name: String): Double = get(name, Options.Real, Value.Double.unapply)
- def update(name: String, x: Double): Options = put(name, Options.Real, Value.Double(x))
- }
- val real = new Real_Access
+ val real: Options.Access[Double] =
+ new Options.Access[Double](this) {
+ def apply(name: String): Double = get(name, Options.Real, Value.Double.unapply)
+ def update(name: String, x: Double): Options = put(name, Options.Real, Value.Double(x))
+ }
- class String_Access extends Options.Access[String] {
- def apply(name: String): String = get(name, Options.String, s => Some(s))
- def update(name: String, x: String): Options = put(name, Options.String, x)
- }
- val string = new String_Access
+ val string: Options.Access[String] =
+ new Options.Access[String](this) {
+ def apply(name: String): String = get(name, Options.String, Some(_))
+ def update(name: String, x: String): Options = put(name, Options.String, x)
+ }
def proper_string(name: String): Option[String] =
Library.proper_string(string(name))
@@ -421,36 +421,35 @@
class Options_Variable(init_options: Options) {
- private var options = init_options
+ private var _options = init_options
- def value: Options = synchronized { options }
+ def value: Options = synchronized { _options }
+ def change(f: Options => Options): Unit = synchronized { _options = f(_options) }
+ def += (name: String, x: String): Unit = change(options => options + (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 extends Options.Access_Variable[Boolean] {
- 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
+ val bool: Options.Access_Variable[Boolean] =
+ new Options.Access_Variable[Boolean](this) {
+ def apply(name: String): Boolean = value.bool(name)
+ def update(name: String, x: Boolean): Unit = change(options => options.bool.update(name, x))
+ }
- class Int_Access extends Options.Access_Variable[Int] {
- 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
+ val int: Options.Access_Variable[Int] =
+ new Options.Access_Variable[Int](this) {
+ def apply(name: String): Int = value.int(name)
+ def update(name: String, x: Int): Unit = change(options => options.int.update(name, x))
+ }
- class Real_Access extends Options.Access_Variable[Double] {
- 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
+ val real: Options.Access_Variable[Double] =
+ new Options.Access_Variable[Double](this) {
+ def apply(name: String): Double = value.real(name)
+ def update(name: String, x: Double): Unit = change(options => options.real.update(name, x))
+ }
- class String_Access extends Options.Access_Variable[String] {
- 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
+ val string: Options.Access_Variable[String] =
+ new Options.Access_Variable[String](this) {
+ def apply(name: String): String = value.string(name)
+ def update(name: String, x: String): Unit = change(options => options.string.update(name, x))
+ }
def proper_string(name: String): Option[String] =
Library.proper_string(string(name))