1.1 --- a/doc-src/IsarRef/Thy/Outer_Syntax.thy	Fri Oct 29 23:15:01 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy	Sat Oct 30 15:26:40 2010 +0200
     1.3 @@ -108,6 +108,7 @@
     1.4      @{syntax_def longident} & = & @{text "ident("}@{verbatim "."}@{text "ident)\<^sup>+"} \\
     1.5      @{syntax_def symident} & = & @{text "sym\<^sup>+  |  "}@{verbatim "\\"}@{verbatim "<"}@{text ident}@{verbatim ">"} \\
     1.6      @{syntax_def nat} & = & @{text "digit\<^sup>+"} \\
     1.7 +    @{syntax_def float} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}@{text "  |  "}@{verbatim "-"}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
     1.8      @{syntax_def var} & = & @{verbatim "?"}@{text "ident  |  "}@{verbatim "?"}@{text ident}@{verbatim "."}@{text nat} \\
     1.9      @{syntax_def typefree} & = & @{verbatim "'"}@{text ident} \\
    1.10      @{syntax_def typevar} & = & @{verbatim "?"}@{text "typefree  |  "}@{verbatim "?"}@{text typefree}@{verbatim "."}@{text nat} \\

     2.1 --- a/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Fri Oct 29 23:15:01 2010 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Sat Oct 30 15:26:40 2010 +0200
     2.3 @@ -127,6 +127,7 @@
     2.4      \indexdef{}{syntax}{longident}\hypertarget{syntax.longident}{\hyperlink{syntax.longident}{\mbox{\isa{longident}}}} & = & \isa{{\isachardoublequote}ident{\isacharparenleft}{\isachardoublequote}}\verb|.|\isa{{\isachardoublequote}ident{\isacharparenright}\isactrlsup {\isacharplus}{\isachardoublequote}} \\
     2.5      \indexdef{}{syntax}{symident}\hypertarget{syntax.symident}{\hyperlink{syntax.symident}{\mbox{\isa{symident}}}} & = & \isa{{\isachardoublequote}sym\isactrlsup {\isacharplus}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|\|\verb|<|\isa{ident}\verb|>| \\
     2.6      \indexdef{}{syntax}{nat}\hypertarget{syntax.nat}{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}} & = & \isa{{\isachardoublequote}digit\isactrlsup {\isacharplus}{\isachardoublequote}} \\
     2.7 +    \indexdef{}{syntax}{float}\hypertarget{syntax.float}{\hyperlink{syntax.float}{\mbox{\isa{float}}}} & = & \indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\verb|.|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|-|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\verb|.|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}} \\
     2.8      \indexdef{}{syntax}{var}\hypertarget{syntax.var}{\hyperlink{syntax.var}{\mbox{\isa{var}}}} & = & \verb|?|\isa{{\isachardoublequote}ident\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|?|\isa{ident}\verb|.|\isa{nat} \\
     2.9      \indexdef{}{syntax}{typefree}\hypertarget{syntax.typefree}{\hyperlink{syntax.typefree}{\mbox{\isa{typefree}}}} & = & \verb|'|\isa{ident} \\
    2.10      \indexdef{}{syntax}{typevar}\hypertarget{syntax.typevar}{\hyperlink{syntax.typevar}{\mbox{\isa{typevar}}}} & = & \verb|?|\isa{{\isachardoublequote}typefree\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|?|\isa{typefree}\verb|.|\isa{nat} \\

     3.1 --- a/src/Pure/General/scan.scala	Fri Oct 29 23:15:01 2010 +0200
     3.2 +++ b/src/Pure/General/scan.scala	Sat Oct 30 15:26:40 2010 +0200
     3.3 @@ -262,6 +262,7 @@
     3.4      {
     3.5        val id = one(symbols.is_letter) ~ many(symbols.is_letdig) ^^ { case x ~ y => x + y }
     3.6        val nat = many1(symbols.is_digit)
     3.7 +      val natdot = nat ~ "." ~ nat ^^ { case x ~ y ~ z => x + y + z }
     3.8        val id_nat = id ~ opt("." ~ nat) ^^ { case x ~ Some(y ~ z) => x + y + z case x ~ None => x }
     3.9  
    3.10        val ident = id ~ rep("." ~> id) ^^
    3.11 @@ -272,6 +273,8 @@
    3.12        val type_ident = "'" ~ id ^^ { case x ~ y => Token(Token.Kind.TYPE_IDENT, x + y) }
    3.13        val type_var = "?'" ~ id_nat ^^ { case x ~ y => Token(Token.Kind.TYPE_VAR, x + y) }
    3.14        val nat_ = nat ^^ (x => Token(Token.Kind.NAT, x))
    3.15 +      val float =
    3.16 +        ("-" ~ natdot ^^ { case x ~ y => x + y } | natdot) ^^ (x => Token(Token.Kind.FLOAT, x))
    3.17  
    3.18        val sym_ident =
    3.19          (many1(symbols.is_symbolic_char) |
    3.20 @@ -294,7 +297,7 @@
    3.21        (space | (string | (alt_string | (verbatim ^^ (x => Token(Token.Kind.VERBATIM, x)) |
    3.22          comment ^^ (x => Token(Token.Kind.COMMENT, x)))))) |
    3.23        bad_delimiter |
    3.24 -      ((ident | (var_ | (type_ident | (type_var | (nat_ | sym_ident))))) |||
    3.25 +      ((ident | (var_ | (type_ident | (type_var | (float | (nat_ | sym_ident)))))) |||
    3.26          keyword ^^ (x => Token(if (is_command(x)) Token.Kind.COMMAND else Token.Kind.KEYWORD, x))) |
    3.27        bad
    3.28      }

     4.1 --- a/src/Pure/Isar/parse.ML	Fri Oct 29 23:15:01 2010 +0200
     4.2 +++ b/src/Pure/Isar/parse.ML	Sat Oct 30 15:26:40 2010 +0200
     4.3 @@ -26,6 +26,7 @@
     4.4    val type_ident: string parser
     4.5    val type_var: string parser
     4.6    val number: string parser
     4.7 +  val float_number: string parser
     4.8    val string: string parser
     4.9    val alt_string: string parser
    4.10    val verbatim: string parser
    4.11 @@ -46,6 +47,7 @@
    4.12    val opt_begin: bool parser
    4.13    val nat: int parser
    4.14    val int: int parser
    4.15 +  val real: real parser
    4.16    val enum: string -> 'a parser -> 'a list parser
    4.17    val enum1: string -> 'a parser -> 'a list parser
    4.18    val and_list: 'a parser -> 'a list parser
    4.19 @@ -168,6 +170,7 @@
    4.20  val type_ident = kind Token.TypeIdent;
    4.21  val type_var = kind Token.TypeVar;
    4.22  val number = kind Token.Nat;
    4.23 +val float_number = kind Token.Float;
    4.24  val string = kind Token.String;
    4.25  val alt_string = kind Token.AltString;
    4.26  val verbatim = kind Token.Verbatim;
    4.27 @@ -192,6 +195,7 @@
    4.28  
    4.29  val nat = number >> (#1 o Library.read_int o Symbol.explode);
    4.30  val int = Scan.optional (minus >> K ~1) 1 -- nat >> op *;
    4.31 +val real = float_number >> (the o Real.fromString);
    4.32  
    4.33  val tag_name = group "tag name" (short_ident || string);
    4.34  val tags = Scan.repeat ($$$ "%" |-- !!! tag_name);

     5.1 --- a/src/Pure/Isar/token.ML	Fri Oct 29 23:15:01 2010 +0200
     5.2 +++ b/src/Pure/Isar/token.ML	Sat Oct 30 15:26:40 2010 +0200
     5.3 @@ -8,7 +8,7 @@
     5.4  sig
     5.5    datatype kind =
     5.6      Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
     5.7 -    Nat | String | AltString | Verbatim | Space | Comment | InternalValue |
     5.8 +    Nat | Float | String | AltString | Verbatim | Space | Comment | InternalValue |
     5.9      Malformed | Error of string | Sync | EOF
    5.10    datatype value =
    5.11      Text of string | Typ of typ | Term of term | Fact of thm list |
    5.12 @@ -89,7 +89,7 @@
    5.13  
    5.14  datatype kind =
    5.15    Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
    5.16 -  Nat | String | AltString | Verbatim | Space | Comment | InternalValue |
    5.17 +  Nat | Float | String | AltString | Verbatim | Space | Comment | InternalValue |
    5.18    Malformed | Error of string | Sync | EOF;
    5.19  
    5.20  datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot;
    5.21 @@ -103,7 +103,8 @@
    5.22    | Var => "schematic variable"
    5.23    | TypeIdent => "type variable"
    5.24    | TypeVar => "schematic type variable"
    5.25 -  | Nat => "number"
    5.26 +  | Nat => "natural number"
    5.27 +  | Float => "floating-point number"
    5.28    | String => "string"
    5.29    | AltString => "back-quoted string"
    5.30    | Verbatim => "verbatim text"
    5.31 @@ -351,6 +352,7 @@
    5.32          Syntax.scan_var >> pair Var ||
    5.33          Syntax.scan_tid >> pair TypeIdent ||
    5.34          Syntax.scan_tvar >> pair TypeVar ||
    5.35 +        Syntax.scan_float >> pair Float ||
    5.36          Syntax.scan_nat >> pair Nat ||
    5.37          scan_symid >> pair SymIdent) >> uncurry token));
    5.38  

     6.1 --- a/src/Pure/Isar/token.scala	Fri Oct 29 23:15:01 2010 +0200
     6.2 +++ b/src/Pure/Isar/token.scala	Sat Oct 30 15:26:40 2010 +0200
     6.3 @@ -21,7 +21,8 @@
     6.4      val VAR = Value("schematic variable")
     6.5      val TYPE_IDENT = Value("type variable")
     6.6      val TYPE_VAR = Value("schematic type variable")
     6.7 -    val NAT = Value("number")
     6.8 +    val NAT = Value("natural number")
     6.9 +    val FLOAT = Value("floating-point number")
    6.10      val STRING = Value("string")
    6.11      val ALT_STRING = Value("back-quoted string")
    6.12      val VERBATIM = Value("verbatim text")

     7.1 --- a/src/Pure/Syntax/lexicon.ML	Fri Oct 29 23:15:01 2010 +0200
     7.2 +++ b/src/Pure/Syntax/lexicon.ML	Sat Oct 30 15:26:40 2010 +0200
     7.3 @@ -14,6 +14,7 @@
     7.4    val scan_tid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
     7.5    val scan_nat: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
     7.6    val scan_int: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
     7.7 +  val scan_float: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
     7.8    val scan_hex: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
     7.9    val scan_bin: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
    7.10    val scan_var: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list

     8.1 --- a/src/Pure/Thy/thy_syntax.ML	Fri Oct 29 23:15:01 2010 +0200
     8.2 +++ b/src/Pure/Thy/thy_syntax.ML	Sat Oct 30 15:26:40 2010 +0200
     8.3 @@ -56,6 +56,7 @@
     8.4    | Token.TypeIdent     => Markup.tfree
     8.5    | Token.TypeVar       => Markup.tvar
     8.6    | Token.Nat           => Markup.ident
     8.7 +  | Token.Float         => Markup.ident
     8.8    | Token.String        => Markup.string
     8.9    | Token.AltString     => Markup.altstring
    8.10    | Token.Verbatim      => Markup.verbatim