exported datatype value;
added the_config;
removed put_generic_src -- moved value parsing to attrib.ML;
tuned;

--- a/src/Pure/config.ML	Fri Jul 27 16:04:26 2007 +0200
+++ b/src/Pure/config.ML	Fri Jul 27 16:31:14 2007 +0200
@@ -8,6 +8,7 @@
 
 signature CONFIG =
 sig
+  datatype value = Bool of bool | Int of int | String of string
   type 'a T
   val get: Proof.context -> 'a T -> 'a
   val get_thy: theory -> 'a T -> 'a
@@ -18,8 +19,8 @@
   val put: 'a T -> 'a -> Proof.context -> Proof.context
   val put_thy: 'a T -> 'a -> theory -> theory
   val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
-  val put_generic_src: string -> string -> Context.generic -> Context.generic
   val print_configs: Proof.context -> unit
+  val the_config: string -> value T * value
   val bool: string -> bool -> bool T
   val int: string -> int -> int T
   val string: string -> string -> string T
@@ -28,6 +29,31 @@
 structure Config: CONFIG =
 struct
 
+(* mixed values *)
+
+datatype value =
+  Bool of bool |
+  Int of int |
+  String of string;
+
+fun print_value (Bool true) = "true"
+  | print_value (Bool false) = "false"
+  | print_value (Int i) = signed_string_of_int i
+  | print_value (String s) = quote s;
+
+fun print_type (Bool _) = "boolean"
+  | print_type (Int _) = "integer"
+  | print_type (String _) = "string";
+
+structure ConfigData = GenericDataFun
+(
+  type T = value Inttab.table;
+  val empty = Inttab.empty;
+  val extend = I;
+  fun merge _ = Inttab.merge (K true);
+);
+
+
 (* abstract configuration options *)
 
 datatype 'a T = Config of
@@ -47,48 +73,21 @@
 fun put_thy config value = map_thy config (K value);
 
 
-(* mixed values *)
-
-datatype value =
-  Bool of bool |
-  Int of int |
-  String of string;
-
-fun read_value (Bool _) "true" = SOME (Bool true)
-  | read_value (Bool _) "false" = SOME (Bool false)
-  | read_value (Int _) s = Option.map Int (Syntax.read_int s)
-  | read_value (String _) s = SOME (String s);
-
-fun print_value (Bool true) = "true"
-  | print_value (Bool false) = "false"
-  | print_value (Int i) = signed_string_of_int i
-  | print_value (String s) = quote s;
-
-fun print_type (Bool _) = "boolean"
-  | print_type (Int _) = "integer"
-  | print_type (String _) = "string";
-
-structure ConfigData = GenericDataFun
-(
-  type T = value Inttab.table;
-  val empty = Inttab.empty;
-  val extend = I;
-  fun merge _ = Inttab.merge (K true);
-);
-
-
 (* global declarations *)
 
 local val global_configs = ref (Symtab.empty: (value T * value) Symtab.table) in
 
-fun put_generic_src name src_value context =
-  (case Symtab.lookup (! global_configs) name of
-    NONE => error ("Unknown configuration option " ^ quote name)
-  | SOME (config, default) =>
-      (case read_value default src_value of
-        SOME value => put_generic config value context
-      | NONE => error ("Malformed " ^ print_type default ^
-          " value for configuration option " ^ quote name)));
+fun print_configs ctxt =
+  let
+    fun prt (name, (config, default)) =
+      Pretty.block [Pretty.str (name ^ ": " ^ print_type default ^ " ="), Pretty.brk 1,
+        Pretty.str (print_value (get_ctxt ctxt config))];
+    val configs = sort_wrt #1 (Symtab.dest (! global_configs));
+  in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;
+
+fun the_config name =
+  (case Symtab.lookup (! global_configs) name of SOME cfg => cfg
+  | NONE => error ("Unknown configuration option " ^ quote name));
 
 fun declare make dest name default =
   let
@@ -107,14 +106,6 @@
 
   in Config {get_value = dest o get_value, map_value = fn f => map_value (make o f o dest)} end;
 
-fun print_configs ctxt =
-  let
-    fun prt (name, (config, default)) =
-      Pretty.block [Pretty.str (name ^ ": " ^ print_type default ^ " ="), Pretty.brk 1,
-        Pretty.str (print_value (get_ctxt ctxt config))];
-    val configs = sort_wrt #1 (Symtab.dest (! global_configs));
-  in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;
-
 end;
 
 val bool = declare Bool (fn Bool b => b);