# HG changeset patch # User wenzelm # Date 1269785609 -7200 # Node ID 5560b2437789429386a9c95ceab3ef601470dec0 # Parent e031755609cffa9b0ad9f2f38fdf40c99f967e4a configuration options admit dynamic default values; diff -r e031755609cf -r 5560b2437789 NEWS --- a/NEWS Sun Mar 28 16:29:51 2010 +0200 +++ b/NEWS Sun Mar 28 16:13:29 2010 +0200 @@ -304,6 +304,9 @@ to emphasize that these only work in a global situation (which is quite rare). +* Configuration options now admit dynamic default values, depending on +the context or even global references. + *** System *** diff -r e031755609cf -r 5560b2437789 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Sun Mar 28 16:29:51 2010 +0200 +++ b/src/Pure/Isar/attrib.ML Sun Mar 28 16:13:29 2010 +0200 @@ -36,12 +36,12 @@ val multi_thm: thm list context_parser val print_configs: Proof.context -> unit val internal: (morphism -> attribute) -> src - val config_bool: bstring -> bool -> bool Config.T * (theory -> theory) - val config_int: bstring -> int -> int Config.T * (theory -> theory) - val config_string: bstring -> string -> string Config.T * (theory -> theory) - val config_bool_global: bstring -> bool -> bool Config.T * (theory -> theory) - val config_int_global: bstring -> int -> int Config.T * (theory -> theory) - val config_string_global: bstring -> string -> string Config.T * (theory -> theory) + val config_bool: bstring -> (Proof.context -> bool) -> bool Config.T * (theory -> theory) + val config_int: bstring -> (Proof.context -> int) -> int Config.T * (theory -> theory) + val config_string: bstring -> (Proof.context -> string) -> string Config.T * (theory -> theory) + val config_bool_global: bstring -> (Proof.context -> bool) -> bool Config.T * (theory -> theory) + val config_int_global: bstring -> (Proof.context -> int) -> int Config.T * (theory -> theory) + val config_string_global: bstring -> (Proof.context -> string) -> string Config.T * (theory -> theory) end; structure Attrib: ATTRIB = @@ -373,7 +373,7 @@ fun declare_config make coerce global name default = let - val config_value = Config.declare global name (make default); + val config_value = Config.declare global name (make o default); val config = coerce config_value; in (config, register_config config_value) end; diff -r e031755609cf -r 5560b2437789 src/Pure/config.ML --- a/src/Pure/config.ML Sun Mar 28 16:29:51 2010 +0200 +++ b/src/Pure/config.ML Sun Mar 28 16:13:29 2010 +0200 @@ -22,7 +22,7 @@ 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 + val declare: bool -> string -> (Proof.context -> value) -> value T val name_of: 'a T -> string end; @@ -102,17 +102,22 @@ 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 get_value context = + (case Inttab.lookup (Value.get context) id of + SOME value => value + | NONE => default (Context.proof_of context)); + + fun update_value f context = + Value.map (Inttab.update (id, type_check name f (get_value context))) context; fun map_value f (context as Context.Proof _) = - let val context' = modify_value f context in + let val context' = update_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; + | map_value f context = update_value f context; in Config {name = name, get_value = get_value, map_value = map_value} end; fun name_of (Config {name, ...}) = name;