src/Pure/System/options.ML

 Stand-alone options with external string representation.
 *)
 
 signature OPTIONS =
 sig
+  val boolT: string
+  val intT: string
+  val realT: string
+  val stringT: string
+  val unknownT: string
   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
   val string: T -> string -> string
+  val put_bool: string -> bool -> T -> T
+  val put_int: string -> int -> T -> T
+  val put_real: string -> real -> T -> T
+  val put_string: string -> string -> T -> T
   val declare: {name: string, typ: string, value: string} -> T -> T
+  val update: string -> 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 default_put_bool: string -> bool -> unit
+  val default_put_int: string -> int -> unit
+  val default_put_real: string -> real -> unit
+  val default_put_string: string -> string -> unit
+  val get_default: string -> string
+  val put_default: string -> string -> unit
   val set_default: T -> unit
   val reset_default: unit -> unit
   val load_default: unit -> unit
 end;
 

 
 val boolT = "bool";
 val intT = "int";
 val realT = "real";
 val stringT = "string";
+val unknownT = "unknown";
 
 datatype T = Options of {typ: string, value: string} Symtab.table;
 
 val empty = Options Symtab.empty;
 
 
+(* check *)
+
+fun check_name (Options tab) name =
+  let val opt = Symtab.lookup tab name in
+    if is_some opt andalso #typ (the opt) <> unknownT then the opt
+    else error ("Unknown option " ^ quote name)
+  end;
+
+fun check_type options name typ =
+  let val opt = check_name options name in
+    if #typ opt = typ then opt
+    else error ("Ill-typed option " ^ quote name ^ " : " ^ #typ opt ^ " vs. " ^ typ)
+  end;
+
+
 (* typ *)
 
-fun typ (Options tab) name =
-  (case Symtab.lookup tab name of
-    SOME opt => #typ opt
-  | NONE => error ("Unknown option " ^ quote name));
+fun typ options name = #typ (check_name options name);
 
 
-(* get *)
+(* basic operations *)
 
-fun get T parse (Options tab) name =
-  (case Symtab.lookup tab name of
-    SOME {typ, value} =>
-      if typ = T then
-        (case parse value of
-          SOME x => x
-        | NONE =>
-            error ("Malformed value for option " ^ quote name ^ " : " ^ T ^ " =\n" ^ quote value))
-      else error ("Ill-typed option " ^ quote name ^ " : " ^ typ ^ " vs. " ^ T)
-  | NONE => error ("Unknown option " ^ quote name));
+fun put T print name x (options as Options tab) =
+  let val opt = check_type options name T
+  in Options (Symtab.update (name, {typ = #typ opt, value = print x}) tab) end;
+
+fun get T parse options name =
+  let val opt = check_type options name T in
+    (case parse (#value opt) of
+      SOME x => x
+    | NONE =>
+        error ("Malformed value for option " ^ quote name ^
+          " : " ^ T ^ " =\n" ^ quote (#value opt)))
+  end;
+
+
+(* internal lookup and update *)
 
 val bool = get boolT Bool.fromString;
 val int = get intT Int.fromString;
 val real = get realT Real.fromString;
 val string = get stringT SOME;
 
+val put_bool = put boolT Bool.toString;
+val put_int = put intT signed_string_of_int;
+val put_real = put realT signed_string_of_real;
+val put_string = put stringT I;
 
-(* declare *)
+
+(* external updates *)
+
+fun check_value options name =
+  let val opt = check_name options name in
+    if #typ opt = boolT then ignore (bool options name)
+    else if #typ opt = intT then ignore (int options name)
+    else if #typ opt = realT then ignore (real options name)
+    else if #typ opt = stringT then ignore (string options name)
+    else ()
+  end;
 
 fun declare {name, typ, value} (Options tab) =
   let
-    val check_value =
-      if typ = boolT then ignore oo bool
-      else if typ = intT then ignore oo int
-      else if typ = realT then ignore oo real
-      else if typ = stringT then ignore oo string
-      else error ("Unknown type for option " ^ quote name ^ " : " ^ quote typ);
     val options' = Options (Symtab.update_new (name, {typ = typ, value = value}) tab)
       handle Symtab.DUP _ => error ("Duplicate declaration of option " ^ quote name);
+    val _ =
+      typ = boolT orelse typ = intT orelse typ = realT orelse typ = stringT orelse
+        error ("Unknown type for option " ^ quote name ^ " : " ^ quote typ);
+    val _ = check_value options' name;
+  in options' end;
+
+fun update name value (options as Options tab) =
+  let
+    val opt = check_name options name;
+    val options' = Options (Symtab.update (name, {typ = #typ opt, value = value}) tab);
     val _ = check_value options' name;
   in options' end;
 
 
 (* decode *)

 
 (** global default **)
 
 val global_default = Synchronized.var "Options.default" (NONE: T option);
 
+fun err_no_default () = error "No global default options";
+
+fun change_default f x y =
+  Synchronized.change global_default
+    (fn SOME options => SOME (f x y options)
+      | NONE => err_no_default ());
+
 fun default () =
   (case Synchronized.value global_default of
     SOME options => options
-  | NONE => error "No global default options");
+  | NONE => err_no_default ());
 
 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;
+
+val default_put_bool = change_default put_bool;
+val default_put_int = change_default put_int;
+val default_put_real = change_default put_real;
+val default_put_string = change_default put_string;
+
+fun get_default name =
+  let val options = default () in get (typ options name) SOME options name end;
+val put_default = change_default update;
 
 fun set_default options = Synchronized.change global_default (K (SOME options));
 fun reset_default () = Synchronized.change global_default (K NONE);
 
 fun load_default () =