src/Pure/System/options.scala
changeset 69073 d05defa39e3d
parent 68841 252b43600737
child 69074 787f3db8e313
equal deleted inserted replaced
69072:337b8ce5ff8d 69073:d05defa39e3d
   278     def apply(name: String): String = get(name, Options.String, s => Some(s))
   278     def apply(name: String): String = get(name, Options.String, s => Some(s))
   279     def update(name: String, x: String): Options = put(name, Options.String, x)
   279     def update(name: String, x: String): Options = put(name, Options.String, x)
   280   }
   280   }
   281   val string = new String_Access
   281   val string = new String_Access
   282 
   282 
   283   class Seconds_Access
   283   def seconds(name: String): Time = Time.seconds(real(name))
   284   {
       
   285     def apply(name: String): Time = Time.seconds(real(name))
       
   286   }
       
   287   val seconds = new Seconds_Access
       
   288 
   284 
   289 
   285 
   290   /* external updates */
   286   /* external updates */
   291 
   287 
   292   private def check_value(name: String): Options =
   288   private def check_value(name: String): Options =
   445     def apply(name: String): String = value.string(name)
   441     def apply(name: String): String = value.string(name)
   446     def update(name: String, x: String): Unit = upd(opts => opts.string.update(name, x))
   442     def update(name: String, x: String): Unit = upd(opts => opts.string.update(name, x))
   447   }
   443   }
   448   val string = new String_Access
   444   val string = new String_Access
   449 
   445 
   450   class Seconds_Access
   446   def seconds(name: String): Time = value.seconds(name)
   451   {
       
   452     def apply(name: String): Time = value.seconds(name)
       
   453   }
       
   454   val seconds = new Seconds_Access
       
   455 }
   447 }