discontinued global config options within attribute name space;
authorwenzelm
Sat May 14 18:29:06 2011 +0200 (2011-05-14)
changeset 4280830870aee8a3f
parent 42807 e639d91d9073
child 42810 2425068fe13a
discontinued global config options within attribute name space;
src/Pure/Isar/attrib.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Sat May 14 17:55:08 2011 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Sat May 14 18:29:06 2011 +0200
     1.3 @@ -44,14 +44,6 @@
     1.4      (Context.generic -> real) -> real Config.T * (theory -> theory)
     1.5    val config_string: Binding.binding ->
     1.6      (Context.generic -> string) -> string Config.T * (theory -> theory)
     1.7 -  val config_bool_global: Binding.binding ->
     1.8 -    (Context.generic -> bool) -> bool Config.T * (theory -> theory)
     1.9 -  val config_int_global: Binding.binding ->
    1.10 -    (Context.generic -> int) -> int Config.T * (theory -> theory)
    1.11 -  val config_real_global: Binding.binding ->
    1.12 -    (Context.generic -> real) -> real Config.T * (theory -> theory)
    1.13 -  val config_string_global: Binding.binding ->
    1.14 -    (Context.generic -> string) -> string Config.T * (theory -> theory)
    1.15    val setup_config_bool: Binding.binding -> (Context.generic -> bool) -> bool Config.T
    1.16    val setup_config_int: Binding.binding -> (Context.generic -> int) -> int Config.T
    1.17    val setup_config_string: Binding.binding -> (Context.generic -> string) -> string Config.T
    1.18 @@ -384,24 +376,19 @@
    1.19      |> Configs.map (Symtab.update (name, config))
    1.20    end;
    1.21  
    1.22 -fun declare make coerce global binding default =
    1.23 +fun declare make coerce binding default =
    1.24    let
    1.25      val name = Binding.name_of binding;
    1.26 -    val config_value = Config.declare_generic {global = global} name (make o default);
    1.27 +    val config_value = Config.declare_generic {global = false} name (make o default);
    1.28      val config = coerce config_value;
    1.29    in (config, register binding config_value) end;
    1.30  
    1.31  in
    1.32  
    1.33 -val config_bool = declare Config.Bool Config.bool false;
    1.34 -val config_int = declare Config.Int Config.int false;
    1.35 -val config_real = declare Config.Real Config.real false;
    1.36 -val config_string = declare Config.String Config.string false;
    1.37 -
    1.38 -val config_bool_global = declare Config.Bool Config.bool true;
    1.39 -val config_int_global = declare Config.Int Config.int true;
    1.40 -val config_real_global = declare Config.Real Config.real true;
    1.41 -val config_string_global = declare Config.String Config.string true;
    1.42 +val config_bool = declare Config.Bool Config.bool;
    1.43 +val config_int = declare Config.Int Config.int;
    1.44 +val config_real = declare Config.Real Config.real;
    1.45 +val config_string = declare Config.String Config.string;
    1.46  
    1.47  fun register_config config = register (Binding.name (Config.name_of config)) config;
    1.48