tuned signature;
authorwenzelm
Thu Jun 27 20:09:39 2013 +0200 (2013-06-27)
changeset 52469c06f1d36a8c9
parent 52468 66b4b60fa69c
child 52470 dedd7952a62c
tuned signature;
src/Pure/config.ML
     1.1 --- a/src/Pure/config.ML	Thu Jun 27 17:36:06 2013 +0200
     1.2 +++ b/src/Pure/config.ML	Thu Jun 27 20:09:39 2013 +0200
     1.3 @@ -24,9 +24,10 @@
     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: string -> (Context.generic -> value) -> raw
     1.8    val declare_global: string -> (Context.generic -> value) -> raw
     1.9 -  val declare: string -> (Context.generic -> value) -> raw
    1.10    val declare_option: string -> raw
    1.11 +  val declare_option_global: string -> raw
    1.12    val name_of: 'a T -> string
    1.13  end;
    1.14  
    1.15 @@ -109,6 +110,8 @@
    1.16    fun merge data = Inttab.merge (K true) data;
    1.17  );
    1.18  
    1.19 +local
    1.20 +
    1.21  fun declare_generic global name default =
    1.22    let
    1.23      val id = serial ();
    1.24 @@ -135,10 +138,7 @@
    1.25        | map_value f context = update_value f context;
    1.26    in Config {name = name, get_value = get_value, map_value = map_value} end;
    1.27  
    1.28 -val declare_global = declare_generic true;
    1.29 -val declare = declare_generic false;
    1.30 -
    1.31 -fun declare_option name =
    1.32 +fun declare_option_generic global name =
    1.33    let
    1.34      val typ = Options.default_typ name;
    1.35      val default =
    1.36 @@ -147,7 +147,16 @@
    1.37        else if typ = Options.realT then fn _ => Real (Options.default_real name)
    1.38        else if typ = Options.stringT then fn _ => String (Options.default_string name)
    1.39        else error ("Unknown type for option " ^ quote name ^ " : " ^ quote typ);
    1.40 -  in declare name default end;
    1.41 +  in declare_generic global name default end;
    1.42 +
    1.43 +in
    1.44 +
    1.45 +val declare = declare_generic false;
    1.46 +val declare_global = declare_generic true;
    1.47 +val declare_option = declare_option_generic false;
    1.48 +val declare_option_global = declare_option_generic true;
    1.49 +
    1.50 +end;
    1.51  
    1.52  fun name_of (Config {name, ...}) = name;
    1.53