src/Pure/config.ML
changeset 24001 067d8e589c58
parent 23987 6d78feed74dd
child 24004 8c962a9be9f2
     1.1 --- a/src/Pure/config.ML	Fri Jul 27 16:04:26 2007 +0200
     1.2 +++ b/src/Pure/config.ML	Fri Jul 27 16:31:14 2007 +0200
     1.3 @@ -8,6 +8,7 @@
     1.4  
     1.5  signature CONFIG =
     1.6  sig
     1.7 +  datatype value = Bool of bool | Int of int | String of string
     1.8    type 'a T
     1.9    val get: Proof.context -> 'a T -> 'a
    1.10    val get_thy: theory -> 'a T -> 'a
    1.11 @@ -18,8 +19,8 @@
    1.12    val put: 'a T -> 'a -> Proof.context -> Proof.context
    1.13    val put_thy: 'a T -> 'a -> theory -> theory
    1.14    val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
    1.15 -  val put_generic_src: string -> string -> Context.generic -> Context.generic
    1.16    val print_configs: Proof.context -> unit
    1.17 +  val the_config: string -> value T * value
    1.18    val bool: string -> bool -> bool T
    1.19    val int: string -> int -> int T
    1.20    val string: string -> string -> string T
    1.21 @@ -28,6 +29,31 @@
    1.22  structure Config: CONFIG =
    1.23  struct
    1.24  
    1.25 +(* mixed values *)
    1.26 +
    1.27 +datatype value =
    1.28 +  Bool of bool |
    1.29 +  Int of int |
    1.30 +  String of string;
    1.31 +
    1.32 +fun print_value (Bool true) = "true"
    1.33 +  | print_value (Bool false) = "false"
    1.34 +  | print_value (Int i) = signed_string_of_int i
    1.35 +  | print_value (String s) = quote s;
    1.36 +
    1.37 +fun print_type (Bool _) = "boolean"
    1.38 +  | print_type (Int _) = "integer"
    1.39 +  | print_type (String _) = "string";
    1.40 +
    1.41 +structure ConfigData = GenericDataFun
    1.42 +(
    1.43 +  type T = value Inttab.table;
    1.44 +  val empty = Inttab.empty;
    1.45 +  val extend = I;
    1.46 +  fun merge _ = Inttab.merge (K true);
    1.47 +);
    1.48 +
    1.49 +
    1.50  (* abstract configuration options *)
    1.51  
    1.52  datatype 'a T = Config of
    1.53 @@ -47,48 +73,21 @@
    1.54  fun put_thy config value = map_thy config (K value);
    1.55  
    1.56  
    1.57 -(* mixed values *)
    1.58 -
    1.59 -datatype value =
    1.60 -  Bool of bool |
    1.61 -  Int of int |
    1.62 -  String of string;
    1.63 -
    1.64 -fun read_value (Bool _) "true" = SOME (Bool true)
    1.65 -  | read_value (Bool _) "false" = SOME (Bool false)
    1.66 -  | read_value (Int _) s = Option.map Int (Syntax.read_int s)
    1.67 -  | read_value (String _) s = SOME (String s);
    1.68 -
    1.69 -fun print_value (Bool true) = "true"
    1.70 -  | print_value (Bool false) = "false"
    1.71 -  | print_value (Int i) = signed_string_of_int i
    1.72 -  | print_value (String s) = quote s;
    1.73 -
    1.74 -fun print_type (Bool _) = "boolean"
    1.75 -  | print_type (Int _) = "integer"
    1.76 -  | print_type (String _) = "string";
    1.77 -
    1.78 -structure ConfigData = GenericDataFun
    1.79 -(
    1.80 -  type T = value Inttab.table;
    1.81 -  val empty = Inttab.empty;
    1.82 -  val extend = I;
    1.83 -  fun merge _ = Inttab.merge (K true);
    1.84 -);
    1.85 -
    1.86 -
    1.87  (* global declarations *)
    1.88  
    1.89  local val global_configs = ref (Symtab.empty: (value T * value) Symtab.table) in
    1.90  
    1.91 -fun put_generic_src name src_value context =
    1.92 -  (case Symtab.lookup (! global_configs) name of
    1.93 -    NONE => error ("Unknown configuration option " ^ quote name)
    1.94 -  | SOME (config, default) =>
    1.95 -      (case read_value default src_value of
    1.96 -        SOME value => put_generic config value context
    1.97 -      | NONE => error ("Malformed " ^ print_type default ^
    1.98 -          " value for configuration option " ^ quote name)));
    1.99 +fun print_configs ctxt =
   1.100 +  let
   1.101 +    fun prt (name, (config, default)) =
   1.102 +      Pretty.block [Pretty.str (name ^ ": " ^ print_type default ^ " ="), Pretty.brk 1,
   1.103 +        Pretty.str (print_value (get_ctxt ctxt config))];
   1.104 +    val configs = sort_wrt #1 (Symtab.dest (! global_configs));
   1.105 +  in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;
   1.106 +
   1.107 +fun the_config name =
   1.108 +  (case Symtab.lookup (! global_configs) name of SOME cfg => cfg
   1.109 +  | NONE => error ("Unknown configuration option " ^ quote name));
   1.110  
   1.111  fun declare make dest name default =
   1.112    let
   1.113 @@ -107,14 +106,6 @@
   1.114  
   1.115    in Config {get_value = dest o get_value, map_value = fn f => map_value (make o f o dest)} end;
   1.116  
   1.117 -fun print_configs ctxt =
   1.118 -  let
   1.119 -    fun prt (name, (config, default)) =
   1.120 -      Pretty.block [Pretty.str (name ^ ": " ^ print_type default ^ " ="), Pretty.brk 1,
   1.121 -        Pretty.str (print_value (get_ctxt ctxt config))];
   1.122 -    val configs = sort_wrt #1 (Symtab.dest (! global_configs));
   1.123 -  in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;
   1.124 -
   1.125  end;
   1.126  
   1.127  val bool = declare Bool (fn Bool b => b);