syntax category "real" subsumes plain "int";
authorwenzelm
Sun Oct 31 13:26:37 2010 +0100 (2010-10-31 ago)
changeset 40296ac4d75f86d97
parent 40295 d4923a7f42c1
child 40297 c753e3f8b4d6
child 40303 2d507370e879
syntax category "real" subsumes plain "int";
doc-src/IsarImplementation/Thy/Prelim.thy
doc-src/IsarImplementation/Thy/document/Prelim.tex
doc-src/IsarRef/Thy/Outer_Syntax.thy
doc-src/IsarRef/Thy/document/Outer_Syntax.tex
src/Pure/Isar/parse.ML
     1.1 --- a/doc-src/IsarImplementation/Thy/Prelim.thy	Sun Oct 31 11:45:45 2010 +0100
     1.2 +++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Sun Oct 31 13:26:37 2010 +0100
     1.3 @@ -663,6 +663,7 @@
     1.4  *}
     1.5  setup airspeed_velocity_setup
     1.6  
     1.7 +declare [[airspeed_velocity = 10]]
     1.8  declare [[airspeed_velocity = 9.9]]
     1.9  
    1.10  
     2.1 --- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Sun Oct 31 11:45:45 2010 +0100
     2.2 +++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Sun Oct 31 13:26:37 2010 +0100
     2.3 @@ -1047,6 +1047,8 @@
     2.4  \isanewline
     2.5  \isanewline
     2.6  \isacommand{declare}\isamarkupfalse%
     2.7 +\ {\isacharbrackleft}{\isacharbrackleft}airspeed{\isacharunderscore}velocity\ {\isacharequal}\ {\isadigit{1}}{\isadigit{0}}{\isacharbrackright}{\isacharbrackright}\isanewline
     2.8 +\isacommand{declare}\isamarkupfalse%
     2.9  \ {\isacharbrackleft}{\isacharbrackleft}airspeed{\isacharunderscore}velocity\ {\isacharequal}\ {\isadigit{9}}{\isachardot}{\isadigit{9}}{\isacharbrackright}{\isacharbrackright}%
    2.10  \isamarkupsection{Names \label{sec:names}%
    2.11  }
     3.1 --- a/doc-src/IsarRef/Thy/Outer_Syntax.thy	Sun Oct 31 11:45:45 2010 +0100
     3.2 +++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy	Sun Oct 31 13:26:37 2010 +0100
     3.3 @@ -197,7 +197,6 @@
     3.4    \railqtok{nameref}.
     3.5  
     3.6    \indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref}
     3.7 -  \indexoutertoken{int}
     3.8    \begin{rail}
     3.9      name: ident | symident | string | nat
    3.10      ;
    3.11 @@ -205,9 +204,26 @@
    3.12      ;
    3.13      nameref: name | longident
    3.14      ;
    3.15 +  \end{rail}
    3.16 +*}
    3.17 +
    3.18 +
    3.19 +subsection {* Numbers *}
    3.20 +
    3.21 +text {* The outer lexical syntax (\secref{sec:outer-lex}) admits
    3.22 +  natural numbers and floating point numbers.  These are combined as
    3.23 +  @{syntax int} and @{syntax real} as follows.
    3.24 +
    3.25 +  \indexoutertoken{int}\indexoutertoken{real}
    3.26 +  \begin{rail}
    3.27      int: nat | '-' nat
    3.28      ;
    3.29 +    real: float | int
    3.30 +    ;
    3.31    \end{rail}
    3.32 +
    3.33 +  Note that there is an overlap with the category \railqtok{name},
    3.34 +  which also includes @{syntax nat}.
    3.35  *}
    3.36  
    3.37  
     4.1 --- a/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Sun Oct 31 11:45:45 2010 +0100
     4.2 +++ b/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Sun Oct 31 13:26:37 2010 +0100
     4.3 @@ -216,7 +216,6 @@
     4.4    \railqtok{nameref}.
     4.5  
     4.6    \indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref}
     4.7 -  \indexoutertoken{int}
     4.8    \begin{rail}
     4.9      name: ident | symident | string | nat
    4.10      ;
    4.11 @@ -224,9 +223,29 @@
    4.12      ;
    4.13      nameref: name | longident
    4.14      ;
    4.15 +  \end{rail}%
    4.16 +\end{isamarkuptext}%
    4.17 +\isamarkuptrue%
    4.18 +%
    4.19 +\isamarkupsubsection{Numbers%
    4.20 +}
    4.21 +\isamarkuptrue%
    4.22 +%
    4.23 +\begin{isamarkuptext}%
    4.24 +The outer lexical syntax (\secref{sec:outer-lex}) admits
    4.25 +  natural numbers and floating point numbers.  These are combined as
    4.26 +  \hyperlink{syntax.int}{\mbox{\isa{int}}} and \hyperlink{syntax.real}{\mbox{\isa{real}}} as follows.
    4.27 +
    4.28 +  \indexoutertoken{int}\indexoutertoken{real}
    4.29 +  \begin{rail}
    4.30      int: nat | '-' nat
    4.31      ;
    4.32 -  \end{rail}%
    4.33 +    real: float | int
    4.34 +    ;
    4.35 +  \end{rail}
    4.36 +
    4.37 +  Note that there is an overlap with the category \railqtok{name},
    4.38 +  which also includes \hyperlink{syntax.nat}{\mbox{\isa{nat}}}.%
    4.39  \end{isamarkuptext}%
    4.40  \isamarkuptrue%
    4.41  %
     5.1 --- a/src/Pure/Isar/parse.ML	Sun Oct 31 11:45:45 2010 +0100
     5.2 +++ b/src/Pure/Isar/parse.ML	Sun Oct 31 13:26:37 2010 +0100
     5.3 @@ -195,7 +195,7 @@
     5.4  
     5.5  val nat = number >> (#1 o Library.read_int o Symbol.explode);
     5.6  val int = Scan.optional (minus >> K ~1) 1 -- nat >> op *;
     5.7 -val real = float_number >> (the o Real.fromString);
     5.8 +val real = float_number >> (the o Real.fromString) || int >> Real.fromInt;
     5.9  
    5.10  val tag_name = group "tag name" (short_ident || string);
    5.11  val tags = Scan.repeat ($$$ "%" |-- !!! tag_name);