# HG changeset patch # User wenzelm # Date 1185980141 -7200 # Node ID ec9e75a46e164d06f630d18b565b145a24df3f5f # Parent 6c4e7d17f9b078e32ed6d5f38cb4ca46fb39d4f7 renamed config_option.ML to config.ML; diff -r 6c4e7d17f9b0 -r ec9e75a46e16 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Wed Aug 01 16:55:40 2007 +0200 +++ b/src/Pure/IsaMakefile Wed Aug 01 16:55:41 2007 +0200 @@ -63,7 +63,7 @@ Tools/codegen_package.ML Tools/codegen_serializer.ML Tools/codegen_thingol.ML \ Tools/invoke.ML Tools/named_thms.ML Tools/nbe.ML Tools/nbe_codegen.ML \ Tools/nbe_eval.ML Tools/xml.ML Tools/xml_syntax.ML assumption.ML axclass.ML \ - codegen.ML compress.ML config_option.ML conjunction.ML consts.ML context.ML \ + codegen.ML compress.ML config.ML conjunction.ML consts.ML context.ML \ context_position.ML conv.ML defs.ML display.ML drule.ML envir.ML \ fact_index.ML goal.ML library.ML logic.ML meta_simplifier.ML \ more_thm.ML morphism.ML name.ML net.ML old_goals.ML pattern.ML proofterm.ML \ diff -r 6c4e7d17f9b0 -r ec9e75a46e16 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Wed Aug 01 16:55:40 2007 +0200 +++ b/src/Pure/ROOT.ML Wed Aug 01 16:55:41 2007 +0200 @@ -27,6 +27,7 @@ use "type.ML"; use "context.ML"; use "context_position.ML"; +use "config.ML"; use "compress.ML"; use "type_infer.ML"; @@ -48,7 +49,6 @@ use "logic.ML"; use "consts.ML"; use "sign.ML"; -use "config_option.ML"; use "pattern.ML"; use "unify.ML"; use "net.ML"; diff -r 6c4e7d17f9b0 -r ec9e75a46e16 src/Pure/config_option.ML --- a/src/Pure/config_option.ML Wed Aug 01 16:55:40 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,164 +0,0 @@ -(* Title: Pure/config_option.ML - ID: $Id$ - Author: Makarius - -Configuration options as values within the local context. Global -environment of named options, with type declaration. -*) - -signature CONFIG_OPTION = -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 - val get_generic: Context.generic -> 'a T -> 'a - val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context - val map_thy: 'a T -> ('a -> 'a) -> theory -> theory - val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic - 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 print_options: Proof.context -> unit - val the_option: theory -> xstring -> value T * value - val bool: string -> bool -> bool T * (theory -> theory) - val int: string -> int -> int T * (theory -> theory) - val string: string -> string -> string T * (theory -> theory) - val global_bool: string -> bool -> bool T * (theory -> theory) - val global_int: string -> int -> int T * (theory -> theory) - val global_string: string -> string -> string T * (theory -> theory) -end; - -structure ConfigOption: CONFIG_OPTION = -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 f value = - let - val value' = f value; - val _ = same_type value value' orelse - error ("Ill-typed configuration option: " ^ print_type value ^ - " expected,\nbut " ^ print_type value' ^ " was found"); - in value' end; - - -(* abstract configuration options *) - -datatype 'a T = ConfigOption of - {get_value: Context.generic -> 'a, - map_value: ('a -> 'a) -> Context.generic -> Context.generic}; - -fun get_generic context (ConfigOption {get_value, ...}) = get_value context; -fun get_ctxt ctxt = get_generic (Context.Proof ctxt); -fun get_thy thy = get_generic (Context.Theory thy); - -fun map_generic (ConfigOption {map_value, ...}) f context = map_value f context; -fun map_ctxt config f = Context.proof_map (map_generic config f); -fun map_thy config f = Context.theory_map (map_generic config f); - -fun put_generic config value = map_generic config (K value); -fun put_ctxt config value = map_ctxt config (K value); -fun put_thy config value = map_thy config (K value); - - -(* context information *) - -fun err_dup_config name = - error ("Duplicate declaration of configuration option " ^ quote name); - -(*global declarations: name, default value and type*) -structure Declaration = TheoryDataFun -(struct - type T = ((value T * value) * serial) NameSpace.table; - val empty = NameSpace.empty_table; - val copy = I; - val extend = I; - fun merge _ tabs = NameSpace.merge_tables (eq_snd (op =)) tabs - handle Symtab.DUP dup => err_dup_config dup; -end); - -(*local values*) -structure Value = GenericDataFun -( - type T = value Inttab.table; - val empty = Inttab.empty; - val extend = I; - fun merge _ = Inttab.merge (K true); -); - -fun print_options ctxt = - let - val thy = ProofContext.theory_of ctxt; - 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 = NameSpace.extern_table (Declaration.get thy); - in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end; - -fun the_option thy xname = - let val (space, tab) = Declaration.get thy in - (case Symtab.lookup tab (NameSpace.intern space xname) of - SOME (config, _) => config - | NONE => error ("Unknown configuration option " ^ quote xname)) - end; - -fun declare global make dest name default = - let - val id = serial (); - - val default_value = make default; - fun get_value context = the_default default_value (Inttab.lookup (Value.get context) id); - fun modify_value f = Value.map (Inttab.map_default (id, default_value) (type_check 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; - - val config_value = ConfigOption {get_value = get_value, map_value = map_value}; - val config = - ConfigOption {get_value = dest o get_value, map_value = fn f => map_value (make o f o dest)}; - fun setup thy = thy |> Declaration.map (fn tab => - NameSpace.extend_table (Sign.naming_of thy) [(name, ((config_value, default_value), id))] tab - handle Symtab.DUP dup => err_dup_config dup); - in (config, setup) end; - -val bool = declare false Bool (fn Bool b => b); -val int = declare false Int (fn Int i => i); -val string = declare false String (fn String s => s); - -val global_bool = declare true Bool (fn Bool b => b); -val global_int = declare true Int (fn Int i => i); -val global_string = declare true String (fn String s => s); - - -(*final declarations of this structure!*) -val get = get_ctxt; -val map = map_ctxt; -val put = put_ctxt; - -end;