# HG changeset patch
# User wenzelm
# Date 1288445200 -7200
# Node ID 47f572aff50a1a22f0ee17103845820b1d793c93
# Parent  b89dae026bae10a3499a95a020c96293b2d2464c
support for floating-point tokens in outer syntax (coinciding with inner syntax version);

diff -r b89dae026bae -r 47f572aff50a doc-src/IsarRef/Thy/Outer_Syntax.thy
--- a/doc-src/IsarRef/Thy/Outer_Syntax.thy	Fri Oct 29 23:15:01 2010 +0200
+++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy	Sat Oct 30 15:26:40 2010 +0200
@@ -108,6 +108,7 @@
     @{syntax_def longident} & = & @{text "ident("}@{verbatim "."}@{text "ident)\<^sup>+"} \\
     @{syntax_def symident} & = & @{text "sym\<^sup>+  |  "}@{verbatim "\\"}@{verbatim "<"}@{text ident}@{verbatim ">"} \\
     @{syntax_def nat} & = & @{text "digit\<^sup>+"} \\
+    @{syntax_def float} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}@{text "  |  "}@{verbatim "-"}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
     @{syntax_def var} & = & @{verbatim "?"}@{text "ident  |  "}@{verbatim "?"}@{text ident}@{verbatim "."}@{text nat} \\
     @{syntax_def typefree} & = & @{verbatim "'"}@{text ident} \\
     @{syntax_def typevar} & = & @{verbatim "?"}@{text "typefree  |  "}@{verbatim "?"}@{text typefree}@{verbatim "."}@{text nat} \\
diff -r b89dae026bae -r 47f572aff50a doc-src/IsarRef/Thy/document/Outer_Syntax.tex
--- a/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Fri Oct 29 23:15:01 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Sat Oct 30 15:26:40 2010 +0200
@@ -127,6 +127,7 @@
     \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}} \\
     \indexdef{}{syntax}{symident}\hypertarget{syntax.symident}{\hyperlink{syntax.symident}{\mbox{\isa{symident}}}} & = & \isa{{\isachardoublequote}sym\isactrlsup {\isacharplus}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|\|\verb|<|\isa{ident}\verb|>| \\
     \indexdef{}{syntax}{nat}\hypertarget{syntax.nat}{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}} & = & \isa{{\isachardoublequote}digit\isactrlsup {\isacharplus}{\isachardoublequote}} \\
+    \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}}} \\
     \indexdef{}{syntax}{var}\hypertarget{syntax.var}{\hyperlink{syntax.var}{\mbox{\isa{var}}}} & = & \verb|?|\isa{{\isachardoublequote}ident\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|?|\isa{ident}\verb|.|\isa{nat} \\
     \indexdef{}{syntax}{typefree}\hypertarget{syntax.typefree}{\hyperlink{syntax.typefree}{\mbox{\isa{typefree}}}} & = & \verb|'|\isa{ident} \\
     \indexdef{}{syntax}{typevar}\hypertarget{syntax.typevar}{\hyperlink{syntax.typevar}{\mbox{\isa{typevar}}}} & = & \verb|?|\isa{{\isachardoublequote}typefree\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|?|\isa{typefree}\verb|.|\isa{nat} \\
diff -r b89dae026bae -r 47f572aff50a src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Fri Oct 29 23:15:01 2010 +0200
+++ b/src/Pure/General/scan.scala	Sat Oct 30 15:26:40 2010 +0200
@@ -262,6 +262,7 @@
     {
       val id = one(symbols.is_letter) ~ many(symbols.is_letdig) ^^ { case x ~ y => x + y }
       val nat = many1(symbols.is_digit)
+      val natdot = nat ~ "." ~ nat ^^ { case x ~ y ~ z => x + y + z }
       val id_nat = id ~ opt("." ~ nat) ^^ { case x ~ Some(y ~ z) => x + y + z case x ~ None => x }
 
       val ident = id ~ rep("." ~> id) ^^
@@ -272,6 +273,8 @@
       val type_ident = "'" ~ id ^^ { case x ~ y => Token(Token.Kind.TYPE_IDENT, x + y) }
       val type_var = "?'" ~ id_nat ^^ { case x ~ y => Token(Token.Kind.TYPE_VAR, x + y) }
       val nat_ = nat ^^ (x => Token(Token.Kind.NAT, x))
+      val float =
+        ("-" ~ natdot ^^ { case x ~ y => x + y } | natdot) ^^ (x => Token(Token.Kind.FLOAT, x))
 
       val sym_ident =
         (many1(symbols.is_symbolic_char) |
@@ -294,7 +297,7 @@
       (space | (string | (alt_string | (verbatim ^^ (x => Token(Token.Kind.VERBATIM, x)) |
         comment ^^ (x => Token(Token.Kind.COMMENT, x)))))) |
       bad_delimiter |
-      ((ident | (var_ | (type_ident | (type_var | (nat_ | sym_ident))))) |||
+      ((ident | (var_ | (type_ident | (type_var | (float | (nat_ | sym_ident)))))) |||
         keyword ^^ (x => Token(if (is_command(x)) Token.Kind.COMMAND else Token.Kind.KEYWORD, x))) |
       bad
     }
diff -r b89dae026bae -r 47f572aff50a src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Fri Oct 29 23:15:01 2010 +0200
+++ b/src/Pure/Isar/parse.ML	Sat Oct 30 15:26:40 2010 +0200
@@ -26,6 +26,7 @@
   val type_ident: string parser
   val type_var: string parser
   val number: string parser
+  val float_number: string parser
   val string: string parser
   val alt_string: string parser
   val verbatim: string parser
@@ -46,6 +47,7 @@
   val opt_begin: bool parser
   val nat: int parser
   val int: int parser
+  val real: real parser
   val enum: string -> 'a parser -> 'a list parser
   val enum1: string -> 'a parser -> 'a list parser
   val and_list: 'a parser -> 'a list parser
@@ -168,6 +170,7 @@
 val type_ident = kind Token.TypeIdent;
 val type_var = kind Token.TypeVar;
 val number = kind Token.Nat;
+val float_number = kind Token.Float;
 val string = kind Token.String;
 val alt_string = kind Token.AltString;
 val verbatim = kind Token.Verbatim;
@@ -192,6 +195,7 @@
 
 val nat = number >> (#1 o Library.read_int o Symbol.explode);
 val int = Scan.optional (minus >> K ~1) 1 -- nat >> op *;
+val real = float_number >> (the o Real.fromString);
 
 val tag_name = group "tag name" (short_ident || string);
 val tags = Scan.repeat ($$$ "%" |-- !!! tag_name);
diff -r b89dae026bae -r 47f572aff50a src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Fri Oct 29 23:15:01 2010 +0200
+++ b/src/Pure/Isar/token.ML	Sat Oct 30 15:26:40 2010 +0200
@@ -8,7 +8,7 @@
 sig
   datatype kind =
     Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
-    Nat | String | AltString | Verbatim | Space | Comment | InternalValue |
+    Nat | Float | String | AltString | Verbatim | Space | Comment | InternalValue |
     Malformed | Error of string | Sync | EOF
   datatype value =
     Text of string | Typ of typ | Term of term | Fact of thm list |
@@ -89,7 +89,7 @@
 
 datatype kind =
   Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
-  Nat | String | AltString | Verbatim | Space | Comment | InternalValue |
+  Nat | Float | String | AltString | Verbatim | Space | Comment | InternalValue |
   Malformed | Error of string | Sync | EOF;
 
 datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot;
@@ -103,7 +103,8 @@
   | Var => "schematic variable"
   | TypeIdent => "type variable"
   | TypeVar => "schematic type variable"
-  | Nat => "number"
+  | Nat => "natural number"
+  | Float => "floating-point number"
   | String => "string"
   | AltString => "back-quoted string"
   | Verbatim => "verbatim text"
@@ -351,6 +352,7 @@
         Syntax.scan_var >> pair Var ||
         Syntax.scan_tid >> pair TypeIdent ||
         Syntax.scan_tvar >> pair TypeVar ||
+        Syntax.scan_float >> pair Float ||
         Syntax.scan_nat >> pair Nat ||
         scan_symid >> pair SymIdent) >> uncurry token));
 
diff -r b89dae026bae -r 47f572aff50a src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Fri Oct 29 23:15:01 2010 +0200
+++ b/src/Pure/Isar/token.scala	Sat Oct 30 15:26:40 2010 +0200
@@ -21,7 +21,8 @@
     val VAR = Value("schematic variable")
     val TYPE_IDENT = Value("type variable")
     val TYPE_VAR = Value("schematic type variable")
-    val NAT = Value("number")
+    val NAT = Value("natural number")
+    val FLOAT = Value("floating-point number")
     val STRING = Value("string")
     val ALT_STRING = Value("back-quoted string")
     val VERBATIM = Value("verbatim text")
diff -r b89dae026bae -r 47f572aff50a src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Fri Oct 29 23:15:01 2010 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Sat Oct 30 15:26:40 2010 +0200
@@ -14,6 +14,7 @@
   val scan_tid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
   val scan_nat: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
   val scan_int: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
+  val scan_float: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
   val scan_hex: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
   val scan_bin: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
   val scan_var: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
diff -r b89dae026bae -r 47f572aff50a src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Fri Oct 29 23:15:01 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.ML	Sat Oct 30 15:26:40 2010 +0200
@@ -56,6 +56,7 @@
   | Token.TypeIdent     => Markup.tfree
   | Token.TypeVar       => Markup.tvar
   | Token.Nat           => Markup.ident
+  | Token.Float         => Markup.ident
   | Token.String        => Markup.string
   | Token.AltString     => Markup.altstring
   | Token.Verbatim      => Markup.verbatim