--- a/src/Pure/Isar/attrib.ML Thu May 16 19:41:41 2013 +0200
+++ b/src/Pure/Isar/attrib.ML Thu May 16 20:33:01 2013 +0200
@@ -57,8 +57,16 @@
(Context.generic -> string) -> string Config.T * (theory -> theory)
val setup_config_bool: Binding.binding -> (Context.generic -> bool) -> bool Config.T
val setup_config_int: Binding.binding -> (Context.generic -> int) -> int Config.T
+ val setup_config_real: Binding.binding -> (Context.generic -> real) -> real Config.T
val setup_config_string: Binding.binding -> (Context.generic -> string) -> string Config.T
- val setup_config_real: Binding.binding -> (Context.generic -> real) -> real Config.T
+ val option_bool: string -> bool Config.T * (theory -> theory)
+ val option_int: string -> int Config.T * (theory -> theory)
+ val option_real: string -> real Config.T * (theory -> theory)
+ val option_string: string -> string Config.T * (theory -> theory)
+ val setup_option_bool: string -> bool Config.T
+ val setup_option_int: string -> int Config.T
+ val setup_option_real: string -> real Config.T
+ val setup_option_string: string -> string Config.T
end;
structure Attrib: ATTRIB =
@@ -482,13 +490,13 @@
in
+fun register_config config = register (Binding.name (Config.name_of config)) config;
+
val config_bool = declare Config.Bool Config.bool;
val config_int = declare Config.Int Config.int;
val config_real = declare Config.Real Config.real;
val config_string = declare Config.String Config.string;
-fun register_config config = register (Binding.name (Config.name_of config)) config;
-
end;
@@ -512,6 +520,36 @@
end;
+(* system options *)
+
+local
+
+fun declare_option coerce name =
+ let
+ val config = Config.declare_option name;
+ in (coerce config, register_config config) end;
+
+fun setup_option coerce name =
+ let
+ val config = Config.declare_option name;
+ val _ = Context.>> (Context.map_theory (register_config config));
+ in coerce config end;
+
+in
+
+val option_bool = declare_option Config.bool;
+val option_int = declare_option Config.int;
+val option_real = declare_option Config.real;
+val option_string = declare_option Config.string;
+
+val setup_option_bool = setup_option Config.bool;
+val setup_option_int = setup_option Config.int;
+val setup_option_real = setup_option Config.real;
+val setup_option_string = setup_option Config.string;
+
+end;
+
+
(* theory setup *)
val _ = Context.>> (Context.map_theory