--- a/NEWS Thu Dec 01 11:54:39 2011 +0100
+++ b/NEWS Thu Dec 01 12:25:27 2011 +0100
@@ -23,6 +23,11 @@
becomes obsolete. Minor INCOMPATIBILITY, due to potential change of
indices of schematic variables.
+* Renamed inner syntax categories "num" to "num_token" and "xnum" to
+"xnum_token", in accordance to existing "float_token". Minor
+INCOMPATIBILITY. Note that in practice "num_const" etc. are mainly
+used instead.
+
*** Pure ***
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Thu Dec 01 11:54:39 2011 +0100
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Thu Dec 01 12:25:27 2011 +0100
@@ -693,24 +693,24 @@
@{syntax_def (inner) var} & = & @{syntax_ref var} \\
@{syntax_def (inner) tid} & = & @{syntax_ref typefree} \\
@{syntax_def (inner) tvar} & = & @{syntax_ref typevar} \\
- @{syntax_def (inner) num} & = & @{syntax_ref nat}@{text " | "}@{verbatim "-"}@{syntax_ref nat} \\
+ @{syntax_def (inner) num_token} & = & @{syntax_ref nat}@{text " | "}@{verbatim "-"}@{syntax_ref nat} \\
@{syntax_def (inner) float_token} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}@{text " | "}@{verbatim "-"}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
- @{syntax_def (inner) xnum} & = & @{verbatim "#"}@{syntax_ref nat}@{text " | "}@{verbatim "#-"}@{syntax_ref nat} \\
+ @{syntax_def (inner) xnum_token} & = & @{verbatim "#"}@{syntax_ref nat}@{text " | "}@{verbatim "#-"}@{syntax_ref nat} \\
@{syntax_def (inner) xstr} & = & @{verbatim "''"} @{text "\<dots>"} @{verbatim "''"} \\
\end{supertabular}
\end{center}
- The token categories @{syntax (inner) num}, @{syntax (inner)
- float_token}, @{syntax (inner) xnum}, and @{syntax (inner) xstr} are
- not used in Pure. Object-logics may implement numerals and string
- constants by adding appropriate syntax declarations, together with
- some translation functions (e.g.\ see Isabelle/HOL).
+ The token categories @{syntax (inner) num_token}, @{syntax (inner)
+ float_token}, @{syntax (inner) xnum_token}, and @{syntax (inner)
+ xstr} are not used in Pure. Object-logics may implement numerals
+ and string constants by adding appropriate syntax declarations,
+ together with some translation functions (e.g.\ see Isabelle/HOL).
- The derived categories @{syntax_def (inner) num_const} and
- @{syntax_def (inner) float_const} provide robust access to @{syntax
- (inner) num}, and @{syntax (inner) float_token}, respectively: the
- syntax tree holds a syntactic constant instead of a free variable.
+ The derived categories @{syntax_def (inner) num_const}, @{syntax_def
+ (inner) float_const}, and @{syntax_def (inner) num_const} provide
+ robust access to the respective tokens: the syntax tree holds a
+ syntactic constant instead of a free variable.
*}
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Thu Dec 01 11:54:39 2011 +0100
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Thu Dec 01 12:25:27 2011 +0100
@@ -866,22 +866,21 @@
\indexdef{inner}{syntax}{var}\hypertarget{syntax.inner.var}{\hyperlink{syntax.inner.var}{\mbox{\isa{var}}}} & = & \indexref{}{syntax}{var}\hyperlink{syntax.var}{\mbox{\isa{var}}} \\
\indexdef{inner}{syntax}{tid}\hypertarget{syntax.inner.tid}{\hyperlink{syntax.inner.tid}{\mbox{\isa{tid}}}} & = & \indexref{}{syntax}{typefree}\hyperlink{syntax.typefree}{\mbox{\isa{typefree}}} \\
\indexdef{inner}{syntax}{tvar}\hypertarget{syntax.inner.tvar}{\hyperlink{syntax.inner.tvar}{\mbox{\isa{tvar}}}} & = & \indexref{}{syntax}{typevar}\hyperlink{syntax.typevar}{\mbox{\isa{typevar}}} \\
- \indexdef{inner}{syntax}{num}\hypertarget{syntax.inner.num}{\hyperlink{syntax.inner.num}{\mbox{\isa{num}}}} & = & \indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\isa{{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|-|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}} \\
+ \indexdef{inner}{syntax}{num\_token}\hypertarget{syntax.inner.num-token}{\hyperlink{syntax.inner.num-token}{\mbox{\isa{num{\isaliteral{5F}{\isacharunderscore}}token}}}} & = & \indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\isa{{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|-|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}} \\
\indexdef{inner}{syntax}{float\_token}\hypertarget{syntax.inner.float-token}{\hyperlink{syntax.inner.float-token}{\mbox{\isa{float{\isaliteral{5F}{\isacharunderscore}}token}}}} & = & \indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\verb|.|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\isa{{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|-|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\verb|.|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}} \\
- \indexdef{inner}{syntax}{xnum}\hypertarget{syntax.inner.xnum}{\hyperlink{syntax.inner.xnum}{\mbox{\isa{xnum}}}} & = & \verb|#|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\isa{{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|#-|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}} \\
+ \indexdef{inner}{syntax}{xnum\_token}\hypertarget{syntax.inner.xnum-token}{\hyperlink{syntax.inner.xnum-token}{\mbox{\isa{xnum{\isaliteral{5F}{\isacharunderscore}}token}}}} & = & \verb|#|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\isa{{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|#-|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}} \\
\indexdef{inner}{syntax}{xstr}\hypertarget{syntax.inner.xstr}{\hyperlink{syntax.inner.xstr}{\mbox{\isa{xstr}}}} & = & \verb|''| \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \verb|''| \\
\end{supertabular}
\end{center}
- The token categories \hyperlink{syntax.inner.num}{\mbox{\isa{num}}}, \hyperlink{syntax.inner.float-token}{\mbox{\isa{float{\isaliteral{5F}{\isacharunderscore}}token}}}, \hyperlink{syntax.inner.xnum}{\mbox{\isa{xnum}}}, and \hyperlink{syntax.inner.xstr}{\mbox{\isa{xstr}}} are
- not used in Pure. Object-logics may implement numerals and string
- constants by adding appropriate syntax declarations, together with
- some translation functions (e.g.\ see Isabelle/HOL).
+ The token categories \hyperlink{syntax.inner.num-token}{\mbox{\isa{num{\isaliteral{5F}{\isacharunderscore}}token}}}, \hyperlink{syntax.inner.float-token}{\mbox{\isa{float{\isaliteral{5F}{\isacharunderscore}}token}}}, \hyperlink{syntax.inner.xnum-token}{\mbox{\isa{xnum{\isaliteral{5F}{\isacharunderscore}}token}}}, and \hyperlink{syntax.inner.xstr}{\mbox{\isa{xstr}}} are not used in Pure. Object-logics may implement numerals
+ and string constants by adding appropriate syntax declarations,
+ together with some translation functions (e.g.\ see Isabelle/HOL).
- The derived categories \indexdef{inner}{syntax}{num\_const}\hypertarget{syntax.inner.num-const}{\hyperlink{syntax.inner.num-const}{\mbox{\isa{num{\isaliteral{5F}{\isacharunderscore}}const}}}} and
- \indexdef{inner}{syntax}{float\_const}\hypertarget{syntax.inner.float-const}{\hyperlink{syntax.inner.float-const}{\mbox{\isa{float{\isaliteral{5F}{\isacharunderscore}}const}}}} provide robust access to \hyperlink{syntax.inner.num}{\mbox{\isa{num}}}, and \hyperlink{syntax.inner.float-token}{\mbox{\isa{float{\isaliteral{5F}{\isacharunderscore}}token}}}, respectively: the
- syntax tree holds a syntactic constant instead of a free variable.%
+ The derived categories \indexdef{inner}{syntax}{num\_const}\hypertarget{syntax.inner.num-const}{\hyperlink{syntax.inner.num-const}{\mbox{\isa{num{\isaliteral{5F}{\isacharunderscore}}const}}}}, \indexdef{inner}{syntax}{float\_const}\hypertarget{syntax.inner.float-const}{\hyperlink{syntax.inner.float-const}{\mbox{\isa{float{\isaliteral{5F}{\isacharunderscore}}const}}}}, and \indexdef{inner}{syntax}{num\_const}\hypertarget{syntax.inner.num-const}{\hyperlink{syntax.inner.num-const}{\mbox{\isa{num{\isaliteral{5F}{\isacharunderscore}}const}}}} provide
+ robust access to the respective tokens: the syntax tree holds a
+ syntactic constant instead of a free variable.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/src/HOL/ex/Numeral.thy Thu Dec 01 11:54:39 2011 +0100
+++ b/src/HOL/ex/Numeral.thy Thu Dec 01 12:25:27 2011 +0100
@@ -274,7 +274,7 @@
*}
syntax
- "_Numerals" :: "xnum \<Rightarrow> 'a" ("_")
+ "_Numerals" :: "xnum_token \<Rightarrow> 'a" ("_")
parse_translation {*
let
--- a/src/Pure/Syntax/lexicon.ML Thu Dec 01 11:54:39 2011 +0100
+++ b/src/Pure/Syntax/lexicon.ML Thu Dec 01 12:25:27 2011 +0100
@@ -177,9 +177,9 @@
("var", VarSy),
("tid", TFreeSy),
("tvar", TVarSy),
- ("num", NumSy),
+ ("num_token", NumSy),
("float_token", FloatSy),
- ("xnum", XNumSy),
+ ("xnum_token", XNumSy),
("xstr", StrSy)];
val terminals = map #1 terminal_kinds;
--- a/src/Pure/Syntax/syntax.ML Thu Dec 01 11:54:39 2011 +0100
+++ b/src/Pure/Syntax/syntax.ML Thu Dec 01 12:25:27 2011 +0100
@@ -547,7 +547,7 @@
val basic_nonterms =
(Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
"args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms",
- "any", "prop'", "num_const", "float_const", "index", "struct",
+ "any", "prop'", "num_const", "float_const", "xnum_const", "index", "struct",
"id_position", "longid_position", "xstr_position", "type_name", "class_name"]);
--- a/src/Pure/pure_thy.ML Thu Dec 01 11:54:39 2011 +0100
+++ b/src/Pure/pure_thy.ML Thu Dec 01 12:25:27 2011 +0100
@@ -125,8 +125,9 @@
("", typ "var => logic", Delimfix "_"),
("_DDDOT", typ "logic", Delimfix "..."),
("_strip_positions", typ "'a", NoSyn),
- ("_constify", typ "num => num_const", Delimfix "_"),
+ ("_constify", typ "num_token => num_const", Delimfix "_"),
("_constify", typ "float_token => float_const", Delimfix "_"),
+ ("_constify", typ "xnum_token => xnum_const", Delimfix "_"),
("_index", typ "logic => index", Delimfix "(00\\<^bsub>_\\<^esub>)"),
("_indexdefault", typ "index", Delimfix ""),
("_indexvar", typ "index", Delimfix "'\\<index>"),
@@ -135,7 +136,7 @@
("_constrainAbs", typ "'a", NoSyn),
("_position", typ "id => id_position", Delimfix "_"),
("_position", typ "longid => longid_position", Delimfix "_"),
- ("_position", typ "xstr => xstr_position", Delimfix "_"),
+ ("_position", typ "xstr => xstr_position", Delimfix "_"),
("_type_constraint_", typ "'a", NoSyn),
("_context_const", typ "id_position => logic", Delimfix "CONST _"),
("_context_const", typ "id_position => aprop", Delimfix "CONST _"),
--- a/src/ZF/Bin.thy Thu Dec 01 11:54:39 2011 +0100
+++ b/src/ZF/Bin.thy Thu Dec 01 12:25:27 2011 +0100
@@ -102,7 +102,7 @@
NCons(bin_mult(v,w),0))"
syntax
- "_Int" :: "xnum => i" ("_")
+ "_Int" :: "xnum_token => i" ("_")
use "Tools/numeral_syntax.ML"
setup Numeral_Syntax.setup