src/Pure/Isar/attrib.ML
changeset 40291 012ed4426fda
parent 39557 fe5722fce758
child 40878 7695e4de4d86
     1.1 --- a/src/Pure/Isar/attrib.ML	Sat Oct 30 15:26:40 2010 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Sat Oct 30 16:33:58 2010 +0200
     1.3 @@ -38,10 +38,13 @@
     1.4    val internal: (morphism -> attribute) -> src
     1.5    val config_bool: bstring -> (Context.generic -> bool) -> bool Config.T * (theory -> theory)
     1.6    val config_int: bstring -> (Context.generic -> int) -> int Config.T * (theory -> theory)
     1.7 +  val config_real: bstring -> (Context.generic -> real) -> real Config.T * (theory -> theory)
     1.8    val config_string: bstring -> (Context.generic -> string) -> string Config.T * (theory -> theory)
     1.9    val config_bool_global: bstring -> (Context.generic -> bool) -> bool Config.T * (theory -> theory)
    1.10    val config_int_global: bstring -> (Context.generic -> int) -> int Config.T * (theory -> theory)
    1.11 -  val config_string_global: bstring -> (Context.generic -> string) -> string Config.T * (theory -> theory)
    1.12 +  val config_real_global: bstring -> (Context.generic -> real) -> real Config.T * (theory -> theory)
    1.13 +  val config_string_global:
    1.14 +    bstring -> (Context.generic -> string) -> string Config.T * (theory -> theory)
    1.15  end;
    1.16  
    1.17  structure Attrib: ATTRIB =
    1.18 @@ -353,6 +356,7 @@
    1.19        equals -- Args.$$$ "true" >> K (Config.Bool true) ||
    1.20        Scan.succeed (Config.Bool true)
    1.21    | scan_value (Config.Int _) = equals |-- Parse.int >> Config.Int
    1.22 +  | scan_value (Config.Real _) = equals |-- Parse.real >> Config.Real
    1.23    | scan_value (Config.String _) = equals |-- Args.name >> Config.String;
    1.24  
    1.25  fun scan_config thy config =
    1.26 @@ -380,10 +384,12 @@
    1.27  
    1.28  val config_bool   = declare_config Config.Bool Config.bool false;
    1.29  val config_int    = declare_config Config.Int Config.int false;
    1.30 +val config_real   = declare_config Config.Real Config.real false;
    1.31  val config_string = declare_config Config.String Config.string false;
    1.32  
    1.33  val config_bool_global   = declare_config Config.Bool Config.bool true;
    1.34  val config_int_global    = declare_config Config.Int Config.int true;
    1.35 +val config_real_global   = declare_config Config.Real Config.real true;
    1.36  val config_string_global = declare_config Config.String Config.string true;
    1.37  
    1.38  end;