src/Pure/Isar/attrib.ML
changeset 52040 852939d19216
parent 52039 d0ba73d11e32
child 52059 2f970c7f722b
     1.1 --- a/src/Pure/Isar/attrib.ML	Thu May 16 19:41:41 2013 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Thu May 16 20:33:01 2013 +0200
     1.3 @@ -57,8 +57,16 @@
     1.4      (Context.generic -> string) -> string Config.T * (theory -> theory)
     1.5    val setup_config_bool: Binding.binding -> (Context.generic -> bool) -> bool Config.T
     1.6    val setup_config_int: Binding.binding -> (Context.generic -> int) -> int Config.T
     1.7 +  val setup_config_real: Binding.binding -> (Context.generic -> real) -> real Config.T
     1.8    val setup_config_string: Binding.binding -> (Context.generic -> string) -> string Config.T
     1.9 -  val setup_config_real: Binding.binding -> (Context.generic -> real) -> real Config.T
    1.10 +  val option_bool: string -> bool Config.T * (theory -> theory)
    1.11 +  val option_int: string -> int Config.T * (theory -> theory)
    1.12 +  val option_real: string -> real Config.T * (theory -> theory)
    1.13 +  val option_string: string -> string Config.T * (theory -> theory)
    1.14 +  val setup_option_bool: string -> bool Config.T
    1.15 +  val setup_option_int: string -> int Config.T
    1.16 +  val setup_option_real: string -> real Config.T
    1.17 +  val setup_option_string: string -> string Config.T
    1.18  end;
    1.19  
    1.20  structure Attrib: ATTRIB =
    1.21 @@ -482,13 +490,13 @@
    1.22  
    1.23  in
    1.24  
    1.25 +fun register_config config = register (Binding.name (Config.name_of config)) config;
    1.26 +
    1.27  val config_bool = declare Config.Bool Config.bool;
    1.28  val config_int = declare Config.Int Config.int;
    1.29  val config_real = declare Config.Real Config.real;
    1.30  val config_string = declare Config.String Config.string;
    1.31  
    1.32 -fun register_config config = register (Binding.name (Config.name_of config)) config;
    1.33 -
    1.34  end;
    1.35  
    1.36  
    1.37 @@ -512,6 +520,36 @@
    1.38  end;
    1.39  
    1.40  
    1.41 +(* system options *)
    1.42 +
    1.43 +local
    1.44 +
    1.45 +fun declare_option coerce name =
    1.46 +  let
    1.47 +    val config = Config.declare_option name;
    1.48 +  in (coerce config, register_config config) end;
    1.49 +
    1.50 +fun setup_option coerce name =
    1.51 +  let
    1.52 +    val config = Config.declare_option name;
    1.53 +    val _ = Context.>> (Context.map_theory (register_config config));
    1.54 +  in coerce config end;
    1.55 +
    1.56 +in
    1.57 +
    1.58 +val option_bool = declare_option Config.bool;
    1.59 +val option_int = declare_option Config.int;
    1.60 +val option_real = declare_option Config.real;
    1.61 +val option_string = declare_option Config.string;
    1.62 +
    1.63 +val setup_option_bool = setup_option Config.bool;
    1.64 +val setup_option_int = setup_option Config.int;
    1.65 +val setup_option_real = setup_option Config.real;
    1.66 +val setup_option_string = setup_option Config.string;
    1.67 +
    1.68 +end;
    1.69 +
    1.70 +
    1.71  (* theory setup *)
    1.72  
    1.73  val _ = Context.>> (Context.map_theory