# HG changeset patch # User wenzelm # Date 1368373356 -7200 # Node ID 3278729bfa3897a94f11c13172ac085df96d5660 # Parent 527e39becafc7b9b3a3c27e62f5ebf5a85c4a4a4 more operations in accordance to Scala version; diff -r 527e39becafc -r 3278729bfa38 src/Pure/System/options.ML --- 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);