--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/config.ML Wed Aug 01 16:55:42 2007 +0200
@@ -0,0 +1,121 @@
+(* Title: Pure/config.ML
+ ID: $Id$
+ Author: Makarius
+
+Configuration options as values within the local context.
+*)
+
+signature CONFIG =
+sig
+ datatype value = Bool of bool | Int of int | String of string
+ val print_value: value -> string
+ val print_type: value -> string
+ type 'a T
+ val bool: value T -> bool T
+ val int: value T -> int T
+ val string: value T -> string T
+ val get: Proof.context -> 'a T -> 'a
+ val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context
+ val put: 'a T -> 'a -> Proof.context -> Proof.context
+ val get_thy: theory -> 'a T -> 'a
+ val map_thy: 'a T -> ('a -> 'a) -> theory -> theory
+ val put_thy: 'a T -> 'a -> theory -> theory
+ val get_generic: Context.generic -> 'a T -> 'a
+ val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
+ val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
+ val declare: bool -> string -> value -> value T
+end;
+
+structure Config: CONFIG =
+struct
+
+(* simple 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";
+
+fun same_type (Bool _) (Bool _) = true
+ | same_type (Int _) (Int _) = true
+ | same_type (String _) (String _) = true
+ | same_type _ _ = false;
+
+fun type_check name f value =
+ let
+ val value' = f value;
+ val _ = same_type value value' orelse
+ error ("Ill-typed configuration option " ^ quote name ^ ": " ^
+ print_type value ^ " expected,\nbut " ^ print_type value' ^ " was found");
+ in value' end;
+
+
+(* abstract configuration options *)
+
+datatype 'a T = Config of
+ {get_value: Context.generic -> 'a,
+ map_value: ('a -> 'a) -> Context.generic -> Context.generic};
+
+fun coerce make dest (Config {get_value, map_value}) =
+ Config {get_value = dest o get_value, map_value = fn f => map_value (make o f o dest)};
+
+val bool = coerce Bool (fn Bool b => b);
+val int = coerce Int (fn Int i => i);
+val string = coerce String (fn String s => s);
+
+fun get_generic context (Config {get_value, ...}) = get_value context;
+fun map_generic (Config {map_value, ...}) f context = map_value f context;
+fun put_generic config value = map_generic config (K value);
+
+fun get_ctxt ctxt = get_generic (Context.Proof ctxt);
+fun map_ctxt config f = Context.proof_map (map_generic config f);
+fun put_ctxt config value = map_ctxt config (K value);
+
+fun get_thy thy = get_generic (Context.Theory thy);
+fun map_thy config f = Context.theory_map (map_generic config f);
+fun put_thy config value = map_thy config (K value);
+
+
+(* context information *)
+
+structure Value = GenericDataFun
+(
+ type T = value Inttab.table;
+ val empty = Inttab.empty;
+ val extend = I;
+ fun merge _ = Inttab.merge (K true);
+);
+
+fun declare global name default =
+ let
+ val id = serial ();
+
+ fun get_value context = the_default default (Inttab.lookup (Value.get context) id);
+ fun modify_value f = Value.map (Inttab.map_default (id, default) (type_check name f));
+
+ fun map_value f (context as Context.Proof _) =
+ let val context' = modify_value f context in
+ if global andalso
+ get_value (Context.Theory (Context.theory_of context')) <> get_value context'
+ then (warning ("Ignoring local change of global option " ^ quote name); context)
+ else context'
+ end
+ | map_value f context = modify_value f context;
+ in Config {get_value = get_value, map_value = map_value} end;
+
+
+(*final declarations of this structure!*)
+val get = get_ctxt;
+val map = map_ctxt;
+val put = put_ctxt;
+
+end;