--- a/src/Pure/System/options.ML Sun May 12 15:08:11 2013 +0200
+++ b/src/Pure/System/options.ML Sun May 12 17:42:36 2013 +0200
@@ -6,6 +6,11 @@
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
@@ -13,13 +18,24 @@
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
@@ -34,51 +50,87 @@
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;
-(* typ *)
+(* check *)
-fun typ (Options tab) name =
- (case Symtab.lookup tab name of
- SOME opt => #typ opt
- | NONE => error ("Unknown option " ^ quote name));
+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;
-(* get *)
+(* typ *)
+
+fun typ options name = #typ (check_name options name);
+
+
+(* basic operations *)
+
+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 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 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;
@@ -95,16 +147,32 @@
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);