src/Pure/config.ML
changeset 39116 f14735a88886
parent 38804 99cc7e748ab4
child 39163 4d701c0388c3
     1.1 --- a/src/Pure/config.ML	Fri Sep 03 15:54:03 2010 +0200
     1.2 +++ b/src/Pure/config.ML	Fri Sep 03 16:09:12 2010 +0200
     1.3 @@ -22,7 +22,9 @@
     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 -> (Context.generic -> value) -> value T
     1.8 +  val declare_generic: {global: bool} -> string -> (Context.generic -> value) -> value T
     1.9 +  val declare_global: string -> (Context.generic -> value) -> value T
    1.10 +  val declare: string -> (Context.generic -> value) -> value T
    1.11    val name_of: 'a T -> string
    1.12  end;
    1.13  
    1.14 @@ -98,7 +100,7 @@
    1.15    fun merge data = Inttab.merge (K true) data;
    1.16  );
    1.17  
    1.18 -fun declare global name default =
    1.19 +fun declare_generic {global} name default =
    1.20    let
    1.21      val id = serial ();
    1.22  
    1.23 @@ -120,6 +122,9 @@
    1.24        | map_value f context = update_value f context;
    1.25    in Config {name = name, get_value = get_value, map_value = map_value} end;
    1.26  
    1.27 +val declare_global = declare_generic {global = true};
    1.28 +val declare = declare_generic {global = false};
    1.29 +
    1.30  fun name_of (Config {name, ...}) = name;
    1.31  
    1.32