src/Pure/System/options.ML
author wenzelm
Thu Aug 02 12:36:54 2012 +0200 (2012-08-02)
changeset 48646 91281e9472d8
parent 48456 d8ff14f44a40
child 48698 2585042b1a30
permissions -rw-r--r--
more official command specifications, including source position;
     1 (*  Title:      Pure/System/options.ML
     2     Author:     Makarius
     3 
     4 Stand-alone options with external string representation.
     5 *)
     6 
     7 signature OPTIONS =
     8 sig
     9   type T
    10   val empty: T
    11   val bool: T -> string -> bool
    12   val int: T -> string -> int
    13   val real: T -> string -> real
    14   val string: T -> string -> string
    15   val declare: {name: string, typ: string, value: string} -> T -> T
    16   val decode: XML.body -> T
    17 end;
    18 
    19 structure Options: OPTIONS =
    20 struct
    21 
    22 (* representation *)
    23 
    24 val boolT = "bool";
    25 val intT = "int";
    26 val realT = "real";
    27 val stringT = "string";
    28 
    29 datatype T = Options of {typ: string, value: string} Symtab.table;
    30 
    31 val empty = Options Symtab.empty;
    32 
    33 
    34 (* get *)
    35 
    36 fun get T parse (Options tab) name =
    37   (case Symtab.lookup tab name of
    38     SOME {typ, value} =>
    39       if typ = T then
    40         (case parse value of
    41           SOME x => x
    42         | NONE =>
    43             error ("Malformed value for option " ^ quote name ^ " : " ^ T ^ " =\n" ^ quote value))
    44       else error ("Ill-typed option " ^ quote name ^ " : " ^ typ ^ " vs. " ^ T)
    45   | NONE => error ("Unknown option " ^ quote name));
    46 
    47 val bool = get boolT Bool.fromString;
    48 val int = get intT Int.fromString;
    49 val real = get realT Real.fromString;
    50 val string = get stringT SOME;
    51 
    52 
    53 (* declare *)
    54 
    55 fun declare {name, typ, value} (Options tab) =
    56   let
    57     val check_value =
    58       if typ = boolT then ignore oo bool
    59       else if typ = intT then ignore oo int
    60       else if typ = realT then ignore oo real
    61       else if typ = stringT then ignore oo string
    62       else error ("Unknown type for option " ^ quote name ^ " : " ^ quote typ);
    63     val options' = Options (Symtab.update_new (name, {typ = typ, value = value}) tab)
    64       handle Symtab.DUP _ => error ("Duplicate declaration of option " ^ quote name);
    65     val _ = check_value options' name;
    66   in options' end;
    67 
    68 
    69 (* decode *)
    70 
    71 fun decode body =
    72   fold (declare o (fn (name, typ, value) => {name = name, typ = typ, value = value}))
    73     (let open XML.Decode in list (triple string string string) end body) empty;
    74 
    75 end;
    76