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
 }