src/Pure/Isar/parse.ML
changeset 40290 47f572aff50a
parent 36959 f5417836dbea
child 40296 ac4d75f86d97
     1.1 --- a/src/Pure/Isar/parse.ML	Fri Oct 29 23:15:01 2010 +0200
     1.2 +++ b/src/Pure/Isar/parse.ML	Sat Oct 30 15:26:40 2010 +0200
     1.3 @@ -26,6 +26,7 @@
     1.4    val type_ident: string parser
     1.5    val type_var: string parser
     1.6    val number: string parser
     1.7 +  val float_number: string parser
     1.8    val string: string parser
     1.9    val alt_string: string parser
    1.10    val verbatim: string parser
    1.11 @@ -46,6 +47,7 @@
    1.12    val opt_begin: bool parser
    1.13    val nat: int parser
    1.14    val int: int parser
    1.15 +  val real: real parser
    1.16    val enum: string -> 'a parser -> 'a list parser
    1.17    val enum1: string -> 'a parser -> 'a list parser
    1.18    val and_list: 'a parser -> 'a list parser
    1.19 @@ -168,6 +170,7 @@
    1.20  val type_ident = kind Token.TypeIdent;
    1.21  val type_var = kind Token.TypeVar;
    1.22  val number = kind Token.Nat;
    1.23 +val float_number = kind Token.Float;
    1.24  val string = kind Token.String;
    1.25  val alt_string = kind Token.AltString;
    1.26  val verbatim = kind Token.Verbatim;
    1.27 @@ -192,6 +195,7 @@
    1.28  
    1.29  val nat = number >> (#1 o Library.read_int o Symbol.explode);
    1.30  val int = Scan.optional (minus >> K ~1) 1 -- nat >> op *;
    1.31 +val real = float_number >> (the o Real.fromString);
    1.32  
    1.33  val tag_name = group "tag name" (short_ident || string);
    1.34  val tags = Scan.repeat ($$$ "%" |-- !!! tag_name);