--- a/src/Pure/Isar/attrib.ML Sat Oct 30 15:26:40 2010 +0200
+++ b/src/Pure/Isar/attrib.ML Sat Oct 30 16:33:58 2010 +0200
@@ -38,10 +38,13 @@
val internal: (morphism -> attribute) -> src
val config_bool: bstring -> (Context.generic -> bool) -> bool Config.T * (theory -> theory)
val config_int: bstring -> (Context.generic -> int) -> int Config.T * (theory -> theory)
+ val config_real: bstring -> (Context.generic -> real) -> real Config.T * (theory -> theory)
val config_string: bstring -> (Context.generic -> string) -> string Config.T * (theory -> theory)
val config_bool_global: bstring -> (Context.generic -> bool) -> bool Config.T * (theory -> theory)
val config_int_global: bstring -> (Context.generic -> int) -> int Config.T * (theory -> theory)
- val config_string_global: bstring -> (Context.generic -> string) -> string Config.T * (theory -> theory)
+ val config_real_global: bstring -> (Context.generic -> real) -> real Config.T * (theory -> theory)
+ val config_string_global:
+ bstring -> (Context.generic -> string) -> string Config.T * (theory -> theory)
end;
structure Attrib: ATTRIB =
@@ -353,6 +356,7 @@
equals -- Args.$$$ "true" >> K (Config.Bool true) ||
Scan.succeed (Config.Bool true)
| scan_value (Config.Int _) = equals |-- Parse.int >> Config.Int
+ | scan_value (Config.Real _) = equals |-- Parse.real >> Config.Real
| scan_value (Config.String _) = equals |-- Args.name >> Config.String;
fun scan_config thy config =
@@ -380,10 +384,12 @@
val config_bool = declare_config Config.Bool Config.bool false;
val config_int = declare_config Config.Int Config.int false;
+val config_real = declare_config Config.Real Config.real false;
val config_string = declare_config Config.String Config.string false;
val config_bool_global = declare_config Config.Bool Config.bool true;
val config_int_global = declare_config Config.Int Config.int true;
+val config_real_global = declare_config Config.Real Config.real true;
val config_string_global = declare_config Config.String Config.string true;
end;