# HG changeset patch
# User wenzelm
# Date 1660395983 -7200
# Node ID a8c401312f9dbb32787f04685e322166ccacb60d
# Parent  7c00d5266bf8d64f90854d20da0452d8a112c844
clarified signature;

diff -r 7c00d5266bf8 -r a8c401312f9d src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Sat Aug 13 14:45:36 2022 +0200
+++ b/src/Pure/System/options.scala	Sat Aug 13 15:06:23 2022 +0200
@@ -13,6 +13,19 @@
   val empty: Options = new Options()
 
 
+  /* access */
+
+  trait Access[A] {
+    def apply(name: String): A
+    def update(name: String, x: A): Options
+  }
+
+  trait Access_Variable[A] {
+    def apply(name: String): A
+    def update(name: String, x: A): Unit
+  }
+
+
   /* representation */
 
   sealed abstract class Type {
@@ -248,28 +261,28 @@
 
   /* internal lookup and update */
 
-  class Bool_Access {
+  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
 
-  class Int_Access {
+  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
 
-  class Real_Access {
+  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
 
-  class String_Access {
+  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)
   }
@@ -414,25 +427,25 @@
   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 {
+  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
 
-  class Int_Access {
+  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
 
-  class Real_Access {
+  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
 
-  class String_Access {
+  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))
   }