--- a/NEWS Tue Feb 14 22:48:07 2012 +0100
+++ b/NEWS Wed Feb 15 13:24:22 2012 +0100
@@ -23,11 +23,15 @@
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 (which also include position information via
-constraints).
+* Renamed some inner syntax categories:
+
+ num ~> num_token
+ xnum ~> xnum_token
+ xstr ~> str_token
+
+Minor INCOMPATIBILITY. Note that in practice "num_const" or
+"num_position" etc. are mainly used instead (which also include
+position information via constraints).
*** Pure ***
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Tue Feb 14 22:48:07 2012 +0100
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Wed Feb 15 13:24:22 2012 +0100
@@ -620,13 +620,13 @@
@{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_token} & = & @{verbatim "#"}@{syntax_ref nat}@{text " | "}@{verbatim "#-"}@{syntax_ref nat} \\
- @{syntax_def (inner) xstr} & = & @{verbatim "''"} @{text "\<dots>"} @{verbatim "''"} \\
+ @{syntax_def (inner) str_token} & = & @{verbatim "''"} @{text "\<dots>"} @{verbatim "''"} \\
\end{supertabular}
\end{center}
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
+ str_token} 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).
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Tue Feb 14 22:48:07 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Wed Feb 15 13:24:22 2012 +0100
@@ -804,11 +804,11 @@
\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\_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|''| \\
+ \indexdef{inner}{syntax}{str\_token}\hypertarget{syntax.inner.str-token}{\hyperlink{syntax.inner.str-token}{\mbox{\isa{str{\isaliteral{5F}{\isacharunderscore}}token}}}} & = & \verb|''| \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \verb|''| \\
\end{supertabular}
\end{center}
- 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
+ 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.str-token}{\mbox{\isa{str{\isaliteral{5F}{\isacharunderscore}}token}}} 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).
--- a/src/HOL/String.thy Tue Feb 14 22:48:07 2012 +0100
+++ b/src/HOL/String.thy Wed Feb 15 13:24:22 2012 +0100
@@ -69,7 +69,7 @@
by (simp add: fun_eq_iff split: char.split)
syntax
- "_Char" :: "xstr_position => char" ("CHR _")
+ "_Char" :: "str_position => char" ("CHR _")
subsection {* Strings *}
@@ -77,7 +77,7 @@
type_synonym string = "char list"
syntax
- "_String" :: "xstr_position => string" ("_")
+ "_String" :: "str_position => string" ("_")
use "Tools/string_syntax.ML"
setup String_Syntax.setup
--- a/src/HOL/Tools/string_syntax.ML Tue Feb 14 22:48:07 2012 +0100
+++ b/src/HOL/Tools/string_syntax.ML Wed Feb 15 13:24:22 2012 +0100
@@ -45,13 +45,13 @@
fun syntax_string cs =
Ast.Appl [Ast.Constant @{syntax_const "_inner_string"},
- Ast.Variable (Lexicon.implode_xstr cs)];
+ Ast.Variable (Lexicon.implode_str cs)];
-fun char_ast_tr [Ast.Variable xstr] =
- (case Lexicon.explode_xstr xstr of
+fun char_ast_tr [Ast.Variable str] =
+ (case Lexicon.explode_str str of
[c] => mk_char c
- | _ => error ("Single character expected: " ^ xstr))
+ | _ => error ("Single character expected: " ^ str))
| char_ast_tr [Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, ast1, ast2]] =
Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, char_ast_tr [ast1], ast2]
| char_ast_tr asts = raise Ast.AST ("char_ast_tr", asts);
@@ -67,8 +67,8 @@
| mk_string (c :: cs) =
Ast.Appl [Ast.Constant @{const_syntax Cons}, mk_char c, mk_string cs];
-fun string_ast_tr [Ast.Variable xstr] =
- (case Lexicon.explode_xstr xstr of
+fun string_ast_tr [Ast.Variable str] =
+ (case Lexicon.explode_str str of
[] =>
Ast.Appl
[Ast.Constant @{syntax_const "_constrain"},
--- a/src/Pure/Syntax/lexicon.ML Tue Feb 14 22:48:07 2012 +0100
+++ b/src/Pure/Syntax/lexicon.ML Wed Feb 15 13:24:22 2012 +0100
@@ -49,8 +49,8 @@
val matching_tokens: token * token -> bool
val valued_token: token -> bool
val predef_term: string -> token option
- val implode_xstr: string list -> string
- val explode_xstr: string -> string list
+ val implode_str: string list -> string
+ val explode_str: string -> string list
val tokenize: Scan.lexicon -> bool -> Symbol_Pos.T list -> token list
val read_indexname: string -> indexname
val read_var: string -> term
@@ -180,7 +180,7 @@
("num_token", NumSy),
("float_token", FloatSy),
("xnum_token", XNumSy),
- ("xstr", StrSy)];
+ ("str_token", StrSy)];
val terminals = map #1 terminal_kinds;
val is_terminal = member (op =) terminals;
@@ -236,7 +236,7 @@
| NONE => NONE);
-(* xstr tokens *)
+(* str tokens *)
val scan_chr =
$$$ "\\" |-- $$$ "'" ||
@@ -254,9 +254,9 @@
((Scan.repeat scan_chr >> flat) --| $$$ "'" --| $$$ "'");
-fun implode_xstr cs = enclose "''" "''" (implode (map (fn "'" => "\\'" | c => c) cs));
+fun implode_str cs = enclose "''" "''" (implode (map (fn "'" => "\\'" | c => c) cs));
-fun explode_xstr str =
+fun explode_str str =
(case Scan.read Symbol_Pos.stopper scan_str_body (Symbol_Pos.explode (str, Position.none)) of
SOME cs => map Symbol_Pos.symbol cs
| _ => error ("Inner lexical error: literal string expected at " ^ quote str));
--- a/src/Pure/Syntax/syntax.ML Tue Feb 14 22:48:07 2012 +0100
+++ b/src/Pure/Syntax/syntax.ML Wed Feb 15 13:24:22 2012 +0100
@@ -544,7 +544,7 @@
"args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms",
"any", "prop'", "num_const", "float_const", "xnum_const", "num_position",
"float_position", "xnum_position", "index", "struct", "id_position",
- "longid_position", "xstr_position", "type_name", "class_name"]);
+ "longid_position", "str_position", "type_name", "class_name"]);
--- a/src/Pure/pure_thy.ML Tue Feb 14 22:48:07 2012 +0100
+++ b/src/Pure/pure_thy.ML Wed Feb 15 13:24:22 2012 +0100
@@ -139,7 +139,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 "str_token => str_position", Delimfix "_"),
("_type_constraint_", typ "'a", NoSyn),
("_context_const", typ "id_position => logic", Delimfix "CONST _"),
("_context_const", typ "id_position => aprop", Delimfix "CONST _"),