# HG changeset patch
# User wenzelm
# Date 1288527997 -3600
# Node ID ac4d75f86d97d6aea40878d47fe194d4245cf01b
# Parent  d4923a7f42c1de4b00a20e7f8915f6624cf4e001
syntax category "real" subsumes plain "int";

diff -r d4923a7f42c1 -r ac4d75f86d97 doc-src/IsarImplementation/Thy/Prelim.thy
--- a/doc-src/IsarImplementation/Thy/Prelim.thy	Sun Oct 31 11:45:45 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Sun Oct 31 13:26:37 2010 +0100
@@ -663,6 +663,7 @@
 *}
 setup airspeed_velocity_setup
 
+declare [[airspeed_velocity = 10]]
 declare [[airspeed_velocity = 9.9]]
 
 
diff -r d4923a7f42c1 -r ac4d75f86d97 doc-src/IsarImplementation/Thy/document/Prelim.tex
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Sun Oct 31 11:45:45 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Sun Oct 31 13:26:37 2010 +0100
@@ -1047,6 +1047,8 @@
 \isanewline
 \isanewline
 \isacommand{declare}\isamarkupfalse%
+\ {\isacharbrackleft}{\isacharbrackleft}airspeed{\isacharunderscore}velocity\ {\isacharequal}\ {\isadigit{1}}{\isadigit{0}}{\isacharbrackright}{\isacharbrackright}\isanewline
+\isacommand{declare}\isamarkupfalse%
 \ {\isacharbrackleft}{\isacharbrackleft}airspeed{\isacharunderscore}velocity\ {\isacharequal}\ {\isadigit{9}}{\isachardot}{\isadigit{9}}{\isacharbrackright}{\isacharbrackright}%
 \isamarkupsection{Names \label{sec:names}%
 }
diff -r d4923a7f42c1 -r ac4d75f86d97 doc-src/IsarRef/Thy/Outer_Syntax.thy
--- a/doc-src/IsarRef/Thy/Outer_Syntax.thy	Sun Oct 31 11:45:45 2010 +0100
+++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy	Sun Oct 31 13:26:37 2010 +0100
@@ -197,7 +197,6 @@
   \railqtok{nameref}.
 
   \indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref}
-  \indexoutertoken{int}
   \begin{rail}
     name: ident | symident | string | nat
     ;
@@ -205,9 +204,26 @@
     ;
     nameref: name | longident
     ;
+  \end{rail}
+*}
+
+
+subsection {* Numbers *}
+
+text {* The outer lexical syntax (\secref{sec:outer-lex}) admits
+  natural numbers and floating point numbers.  These are combined as
+  @{syntax int} and @{syntax real} as follows.
+
+  \indexoutertoken{int}\indexoutertoken{real}
+  \begin{rail}
     int: nat | '-' nat
     ;
+    real: float | int
+    ;
   \end{rail}
+
+  Note that there is an overlap with the category \railqtok{name},
+  which also includes @{syntax nat}.
 *}
 
 
diff -r d4923a7f42c1 -r ac4d75f86d97 doc-src/IsarRef/Thy/document/Outer_Syntax.tex
--- a/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Sun Oct 31 11:45:45 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Sun Oct 31 13:26:37 2010 +0100
@@ -216,7 +216,6 @@
   \railqtok{nameref}.
 
   \indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref}
-  \indexoutertoken{int}
   \begin{rail}
     name: ident | symident | string | nat
     ;
@@ -224,9 +223,29 @@
     ;
     nameref: name | longident
     ;
+  \end{rail}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Numbers%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The outer lexical syntax (\secref{sec:outer-lex}) admits
+  natural numbers and floating point numbers.  These are combined as
+  \hyperlink{syntax.int}{\mbox{\isa{int}}} and \hyperlink{syntax.real}{\mbox{\isa{real}}} as follows.
+
+  \indexoutertoken{int}\indexoutertoken{real}
+  \begin{rail}
     int: nat | '-' nat
     ;
-  \end{rail}%
+    real: float | int
+    ;
+  \end{rail}
+
+  Note that there is an overlap with the category \railqtok{name},
+  which also includes \hyperlink{syntax.nat}{\mbox{\isa{nat}}}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r d4923a7f42c1 -r ac4d75f86d97 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Sun Oct 31 11:45:45 2010 +0100
+++ b/src/Pure/Isar/parse.ML	Sun Oct 31 13:26:37 2010 +0100
@@ -195,7 +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 real = float_number >> (the o Real.fromString) || int >> Real.fromInt;
 
 val tag_name = group "tag name" (short_ident || string);
 val tags = Scan.repeat ($$$ "%" |-- !!! tag_name);