more systematic access to options default;

--- a/src/Pure/ML/ml_antiquote.ML	Sun May 12 15:05:15 2013 +0200
+++ b/src/Pure/ML/ml_antiquote.ML	Sun May 12 15:08:11 2013 +0200
@@ -67,6 +67,10 @@
 
   inline (Binding.name "make_string") (Scan.succeed ml_make_string) #>
 
+  value (Binding.name "option_default") (Scan.lift Args.name >> (fn name =>
+    let val typ = Options.typ (Options.default ()) name
+    in "fn () => Options.default_" ^ typ ^ " " ^ ML_Syntax.print_string name end)) #>
+
   value (Binding.name "binding")
     (Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding) #>
 

--- a/src/Pure/System/options.ML	Sun May 12 15:05:15 2013 +0200
+++ b/src/Pure/System/options.ML	Sun May 12 15:08:11 2013 +0200
@@ -8,6 +8,7 @@
 sig
   type T
   val empty: T
+  val typ: T -> string -> string
   val bool: T -> string -> bool
   val int: T -> string -> int
   val real: T -> string -> real
@@ -15,6 +16,10 @@
   val declare: {name: string, typ: string, value: string} -> T -> T
   val decode: XML.body -> T
   val default: unit -> T
+  val default_bool: string -> bool
+  val default_int: string -> int
+  val default_real: string -> real
+  val default_string: string -> string
   val set_default: T -> unit
   val reset_default: unit -> unit
   val load_default: unit -> unit
@@ -35,6 +40,14 @@
 val empty = Options Symtab.empty;
 
 
+(* typ *)
+
+fun typ (Options tab) name =
+  (case Symtab.lookup tab name of
+    SOME opt => #typ opt
+  | NONE => error ("Unknown option " ^ quote name));
+
+
 (* get *)
 
 fun get T parse (Options tab) name =
@@ -87,6 +100,11 @@
     SOME options => options
   | NONE => error "No global default options");
 
+fun default_bool name = bool (default ()) name;
+fun default_int name = int (default ()) name;
+fun default_real name = real (default ()) name;
+fun default_string name = string (default ()) name;
+
 fun set_default options = Synchronized.change global_default (K (SOME options));
 fun reset_default () = Synchronized.change global_default (K NONE);