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