src/Pure/Isar/attrib.ML
changeset 42616 92715b528e78
parent 42380 9371ea9f91fb
child 42669 04dfffda5671
     1.1 --- a/src/Pure/Isar/attrib.ML	Mon May 02 13:29:47 2011 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Mon May 02 16:33:21 2011 +0200
     1.3 @@ -36,15 +36,26 @@
     1.4    val multi_thm: thm list context_parser
     1.5    val print_configs: Proof.context -> unit
     1.6    val internal: (morphism -> attribute) -> src
     1.7 -  val config_bool: bstring -> (Context.generic -> bool) -> bool Config.T * (theory -> theory)
     1.8 -  val config_int: bstring -> (Context.generic -> int) -> int Config.T * (theory -> theory)
     1.9 -  val config_real: bstring -> (Context.generic -> real) -> real Config.T * (theory -> theory)
    1.10 -  val config_string: bstring -> (Context.generic -> string) -> string Config.T * (theory -> theory)
    1.11 -  val config_bool_global: bstring -> (Context.generic -> bool) -> bool Config.T * (theory -> theory)
    1.12 -  val config_int_global: bstring -> (Context.generic -> int) -> int Config.T * (theory -> theory)
    1.13 -  val config_real_global: bstring -> (Context.generic -> real) -> real Config.T * (theory -> theory)
    1.14 -  val config_string_global:
    1.15 -    bstring -> (Context.generic -> string) -> string Config.T * (theory -> theory)
    1.16 +  val config_bool: Binding.binding ->
    1.17 +    (Context.generic -> bool) -> bool Config.T * (theory -> theory)
    1.18 +  val config_int: Binding.binding ->
    1.19 +    (Context.generic -> int) -> int Config.T * (theory -> theory)
    1.20 +  val config_real: Binding.binding ->
    1.21 +    (Context.generic -> real) -> real Config.T * (theory -> theory)
    1.22 +  val config_string: Binding.binding ->
    1.23 +    (Context.generic -> string) -> string Config.T * (theory -> theory)
    1.24 +  val config_bool_global: Binding.binding ->
    1.25 +    (Context.generic -> bool) -> bool Config.T * (theory -> theory)
    1.26 +  val config_int_global: Binding.binding ->
    1.27 +    (Context.generic -> int) -> int Config.T * (theory -> theory)
    1.28 +  val config_real_global: Binding.binding ->
    1.29 +    (Context.generic -> real) -> real Config.T * (theory -> theory)
    1.30 +  val config_string_global: Binding.binding ->
    1.31 +    (Context.generic -> string) -> string Config.T * (theory -> theory)
    1.32 +  val setup_config_bool: Binding.binding -> (Context.generic -> bool) -> bool Config.T
    1.33 +  val setup_config_int: Binding.binding -> (Context.generic -> int) -> int Config.T
    1.34 +  val setup_config_string: Binding.binding -> (Context.generic -> string) -> string Config.T
    1.35 +  val setup_config_real: Binding.binding -> (Context.generic -> real) -> real Config.T
    1.36  end;
    1.37  
    1.38  structure Attrib: ATTRIB =
    1.39 @@ -366,34 +377,53 @@
    1.40    let val config_type = Config.get_global thy config
    1.41    in scan_value config_type >> (K o Thm.declaration_attribute o K o Config.put_generic config) end;
    1.42  
    1.43 -in
    1.44 -
    1.45 -fun register_config config thy =
    1.46 -  let
    1.47 -    val bname = Config.name_of config;
    1.48 -    val name = Sign.full_bname thy bname;
    1.49 -  in
    1.50 +fun register binding config thy =
    1.51 +  let val name = Sign.full_name thy binding in
    1.52      thy
    1.53 -    |> setup (Binding.name bname) (Scan.lift (scan_config thy config) >> Morphism.form)
    1.54 -      "configuration option"
    1.55 +    |> setup binding (Scan.lift (scan_config thy config) >> Morphism.form) "configuration option"
    1.56      |> Configs.map (Symtab.update (name, config))
    1.57    end;
    1.58  
    1.59 -fun declare_config make coerce global name default =
    1.60 +fun declare make coerce global binding default =
    1.61    let
    1.62 +    val name = Binding.name_of binding;
    1.63      val config_value = Config.declare_generic {global = global} name (make o default);
    1.64      val config = coerce config_value;
    1.65 -  in (config, register_config config_value) end;
    1.66 +  in (config, register binding config_value) end;
    1.67 +
    1.68 +in
    1.69 +
    1.70 +val config_bool = declare Config.Bool Config.bool false;
    1.71 +val config_int = declare Config.Int Config.int false;
    1.72 +val config_real = declare Config.Real Config.real false;
    1.73 +val config_string = declare Config.String Config.string false;
    1.74 +
    1.75 +val config_bool_global = declare Config.Bool Config.bool true;
    1.76 +val config_int_global = declare Config.Int Config.int true;
    1.77 +val config_real_global = declare Config.Real Config.real true;
    1.78 +val config_string_global = declare Config.String Config.string true;
    1.79 +
    1.80 +fun register_config config = register (Binding.name (Config.name_of config)) config;
    1.81 +
    1.82 +end;
    1.83  
    1.84 -val config_bool = declare_config Config.Bool Config.bool false;
    1.85 -val config_int = declare_config Config.Int Config.int false;
    1.86 -val config_real = declare_config Config.Real Config.real false;
    1.87 -val config_string = declare_config Config.String Config.string false;
    1.88 +
    1.89 +(* implicit setup *)
    1.90 +
    1.91 +local
    1.92  
    1.93 -val config_bool_global = declare_config Config.Bool Config.bool true;
    1.94 -val config_int_global = declare_config Config.Int Config.int true;
    1.95 -val config_real_global = declare_config Config.Real Config.real true;
    1.96 -val config_string_global = declare_config Config.String Config.string true;
    1.97 +fun setup_config declare_config binding default =
    1.98 +  let
    1.99 +    val (config, setup) = declare_config binding default;
   1.100 +    val _ = Context.>> (Context.map_theory setup);
   1.101 +  in config end;
   1.102 +
   1.103 +in
   1.104 +
   1.105 +val setup_config_bool = setup_config config_bool;
   1.106 +val setup_config_int = setup_config config_int;
   1.107 +val setup_config_string = setup_config config_string;
   1.108 +val setup_config_real = setup_config config_real;
   1.109  
   1.110  end;
   1.111