src/Pure/config.ML
changeset 36000 5560b2437789
parent 33519 e31a85f92ce9
child 36002 f4f343500249
     1.1 --- a/src/Pure/config.ML	Sun Mar 28 16:29:51 2010 +0200
     1.2 +++ b/src/Pure/config.ML	Sun Mar 28 16:13:29 2010 +0200
     1.3 @@ -22,7 +22,7 @@
     1.4    val get_generic: Context.generic -> 'a T -> 'a
     1.5    val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
     1.6    val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
     1.7 -  val declare: bool -> string -> value -> value T
     1.8 +  val declare: bool -> string -> (Proof.context -> value) -> value T
     1.9    val name_of: 'a T -> string
    1.10  end;
    1.11  
    1.12 @@ -102,17 +102,22 @@
    1.13    let
    1.14      val id = serial ();
    1.15  
    1.16 -    fun get_value context = the_default default (Inttab.lookup (Value.get context) id);
    1.17 -    fun modify_value f = Value.map (Inttab.map_default (id, default) (type_check name f));
    1.18 +    fun get_value context =
    1.19 +      (case Inttab.lookup (Value.get context) id of
    1.20 +        SOME value => value
    1.21 +      | NONE => default (Context.proof_of context));
    1.22 +
    1.23 +    fun update_value f context =
    1.24 +      Value.map (Inttab.update (id, type_check name f (get_value context))) context;
    1.25  
    1.26      fun map_value f (context as Context.Proof _) =
    1.27 -          let val context' = modify_value f context in
    1.28 +          let val context' = update_value f context in
    1.29              if global andalso
    1.30                get_value (Context.Theory (Context.theory_of context')) <> get_value context'
    1.31              then (warning ("Ignoring local change of global option " ^ quote name); context)
    1.32              else context'
    1.33            end
    1.34 -      | map_value f context = modify_value f context;
    1.35 +      | map_value f context = update_value f context;
    1.36    in Config {name = name, get_value = get_value, map_value = map_value} end;
    1.37  
    1.38  fun name_of (Config {name, ...}) = name;