configuration options admit dynamic default values;
authorwenzelm
Sun Mar 28 16:13:29 2010 +0200 (2010-03-28)
changeset 360005560b2437789
parent 35999 e031755609cf
child 36001 992839c4be90
configuration options admit dynamic default values;
NEWS
src/Pure/Isar/attrib.ML
src/Pure/config.ML
     1.1 --- a/NEWS	Sun Mar 28 16:29:51 2010 +0200
     1.2 +++ b/NEWS	Sun Mar 28 16:13:29 2010 +0200
     1.3 @@ -304,6 +304,9 @@
     1.4  to emphasize that these only work in a global situation (which is
     1.5  quite rare).
     1.6  
     1.7 +* Configuration options now admit dynamic default values, depending on
     1.8 +the context or even global references.
     1.9 +
    1.10  
    1.11  *** System ***
    1.12  
     2.1 --- a/src/Pure/Isar/attrib.ML	Sun Mar 28 16:29:51 2010 +0200
     2.2 +++ b/src/Pure/Isar/attrib.ML	Sun Mar 28 16:13:29 2010 +0200
     2.3 @@ -36,12 +36,12 @@
     2.4    val multi_thm: thm list context_parser
     2.5    val print_configs: Proof.context -> unit
     2.6    val internal: (morphism -> attribute) -> src
     2.7 -  val config_bool: bstring -> bool -> bool Config.T * (theory -> theory)
     2.8 -  val config_int: bstring -> int -> int Config.T * (theory -> theory)
     2.9 -  val config_string: bstring -> string -> string Config.T * (theory -> theory)
    2.10 -  val config_bool_global: bstring -> bool -> bool Config.T * (theory -> theory)
    2.11 -  val config_int_global: bstring -> int -> int Config.T * (theory -> theory)
    2.12 -  val config_string_global: bstring -> string -> string Config.T * (theory -> theory)
    2.13 +  val config_bool: bstring -> (Proof.context -> bool) -> bool Config.T * (theory -> theory)
    2.14 +  val config_int: bstring -> (Proof.context -> int) -> int Config.T * (theory -> theory)
    2.15 +  val config_string: bstring -> (Proof.context -> string) -> string Config.T * (theory -> theory)
    2.16 +  val config_bool_global: bstring -> (Proof.context -> bool) -> bool Config.T * (theory -> theory)
    2.17 +  val config_int_global: bstring -> (Proof.context -> int) -> int Config.T * (theory -> theory)
    2.18 +  val config_string_global: bstring -> (Proof.context -> string) -> string Config.T * (theory -> theory)
    2.19  end;
    2.20  
    2.21  structure Attrib: ATTRIB =
    2.22 @@ -373,7 +373,7 @@
    2.23  
    2.24  fun declare_config make coerce global name default =
    2.25    let
    2.26 -    val config_value = Config.declare global name (make default);
    2.27 +    val config_value = Config.declare global name (make o default);
    2.28      val config = coerce config_value;
    2.29    in (config, register_config config_value) end;
    2.30  
     3.1 --- a/src/Pure/config.ML	Sun Mar 28 16:29:51 2010 +0200
     3.2 +++ b/src/Pure/config.ML	Sun Mar 28 16:13:29 2010 +0200
     3.3 @@ -22,7 +22,7 @@
     3.4    val get_generic: Context.generic -> 'a T -> 'a
     3.5    val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
     3.6    val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
     3.7 -  val declare: bool -> string -> value -> value T
     3.8 +  val declare: bool -> string -> (Proof.context -> value) -> value T
     3.9    val name_of: 'a T -> string
    3.10  end;
    3.11  
    3.12 @@ -102,17 +102,22 @@
    3.13    let
    3.14      val id = serial ();
    3.15  
    3.16 -    fun get_value context = the_default default (Inttab.lookup (Value.get context) id);
    3.17 -    fun modify_value f = Value.map (Inttab.map_default (id, default) (type_check name f));
    3.18 +    fun get_value context =
    3.19 +      (case Inttab.lookup (Value.get context) id of
    3.20 +        SOME value => value
    3.21 +      | NONE => default (Context.proof_of context));
    3.22 +
    3.23 +    fun update_value f context =
    3.24 +      Value.map (Inttab.update (id, type_check name f (get_value context))) context;
    3.25  
    3.26      fun map_value f (context as Context.Proof _) =
    3.27 -          let val context' = modify_value f context in
    3.28 +          let val context' = update_value f context in
    3.29              if global andalso
    3.30                get_value (Context.Theory (Context.theory_of context')) <> get_value context'
    3.31              then (warning ("Ignoring local change of global option " ^ quote name); context)
    3.32              else context'
    3.33            end
    3.34 -      | map_value f context = modify_value f context;
    3.35 +      | map_value f context = update_value f context;
    3.36    in Config {name = name, get_value = get_value, map_value = map_value} end;
    3.37  
    3.38  fun name_of (Config {name, ...}) = name;