# HG changeset patch
# User wenzelm
# Date 1459521114 -7200
# Node ID 64ebecf8646c007a04c02e0796e6bfbf6a339e8d
# Parent  0c526d2fb609a99f4e5c662b16799da96e419f33
more operations (cf. Scala version);

diff -r 0c526d2fb609 -r 64ebecf8646c src/Pure/System/options.ML
--- a/src/Pure/System/options.ML	Fri Apr 01 16:20:04 2016 +0200
+++ b/src/Pure/System/options.ML	Fri Apr 01 16:31:54 2016 +0200
@@ -19,6 +19,7 @@
   val bool: T -> string -> bool
   val int: T -> string -> int
   val real: T -> string -> real
+  val seconds: T -> string -> Time.time
   val string: T -> string -> string
   val put_bool: string -> bool -> T -> T
   val put_int: string -> int -> T -> T
@@ -33,6 +34,7 @@
   val default_bool: string -> bool
   val default_int: string -> int
   val default_real: string -> real
+  val default_seconds: string -> Time.time
   val default_string: string -> string
   val default_put_bool: string -> bool -> unit
   val default_put_int: string -> int -> unit
@@ -115,6 +117,7 @@
 val bool = get boolT (try Markup.parse_bool);
 val int = get intT (try Markup.parse_int);
 val real = get realT (try Markup.parse_real);
+val seconds = Time.fromReal oo real;
 val string = get stringT SOME;
 
 val put_bool = put boolT Markup.print_bool;
@@ -191,6 +194,7 @@
 fun default_bool name = bool (default ()) name;
 fun default_int name = int (default ()) name;
 fun default_real name = real (default ()) name;
+fun default_seconds name = seconds (default ()) name;
 fun default_string name = string (default ()) name;
 
 val default_put_bool = change_default put_bool;