1.1 --- a/src/Pure/General/scan.scala	Fri Oct 29 23:15:01 2010 +0200
     1.2 +++ b/src/Pure/General/scan.scala	Sat Oct 30 15:26:40 2010 +0200
     1.3 @@ -262,6 +262,7 @@
     1.4      {
     1.5        val id = one(symbols.is_letter) ~ many(symbols.is_letdig) ^^ { case x ~ y => x + y }
     1.6        val nat = many1(symbols.is_digit)
     1.7 +      val natdot = nat ~ "." ~ nat ^^ { case x ~ y ~ z => x + y + z }
     1.8        val id_nat = id ~ opt("." ~ nat) ^^ { case x ~ Some(y ~ z) => x + y + z case x ~ None => x }
     1.9  
    1.10        val ident = id ~ rep("." ~> id) ^^
    1.11 @@ -272,6 +273,8 @@
    1.12        val type_ident = "'" ~ id ^^ { case x ~ y => Token(Token.Kind.TYPE_IDENT, x + y) }
    1.13        val type_var = "?'" ~ id_nat ^^ { case x ~ y => Token(Token.Kind.TYPE_VAR, x + y) }
    1.14        val nat_ = nat ^^ (x => Token(Token.Kind.NAT, x))
    1.15 +      val float =
    1.16 +        ("-" ~ natdot ^^ { case x ~ y => x + y } | natdot) ^^ (x => Token(Token.Kind.FLOAT, x))
    1.17  
    1.18        val sym_ident =
    1.19          (many1(symbols.is_symbolic_char) |
    1.20 @@ -294,7 +297,7 @@
    1.21        (space | (string | (alt_string | (verbatim ^^ (x => Token(Token.Kind.VERBATIM, x)) |
    1.22          comment ^^ (x => Token(Token.Kind.COMMENT, x)))))) |
    1.23        bad_delimiter |
    1.24 -      ((ident | (var_ | (type_ident | (type_var | (nat_ | sym_ident))))) |||
    1.25 +      ((ident | (var_ | (type_ident | (type_var | (float | (nat_ | sym_ident)))))) |||
    1.26          keyword ^^ (x => Token(if (is_command(x)) Token.Kind.COMMAND else Token.Kind.KEYWORD, x))) |
    1.27        bad
    1.28      }