diff -r 6626bc5ed053 -r 54be125d8cdc src/Pure/System/options.scala --- a/src/Pure/System/options.scala Sun Nov 25 21:10:29 2012 +0100 +++ b/src/Pure/System/options.scala Sun Nov 25 21:23:20 2012 +0100 @@ -229,6 +229,12 @@ } val string = new String_Access + class Seconds_Access + { + def apply(name: String): Time = Time.seconds(real(name)) + } + val seconds = new Seconds_Access + /* external updates */ @@ -410,5 +416,11 @@ } } val string = new String_Access + + class Seconds_Access + { + def apply(name: String): Time = options.seconds(name) + } + val seconds = new Seconds_Access }