configuration options admit dynamic default values;

--- 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 ***
 

--- 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;
 

--- 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;