# HG changeset patch # User wenzelm # Date 1329308662 -3600 # Node ID 10a9c31a22b4790502d36177c19b629b633ef198 # Parent f310e9eabf60eafe00dbf32d5ea3987ee19f6719 renamed "xstr" to "str_token"; diff -r f310e9eabf60 -r 10a9c31a22b4 NEWS --- 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 *** diff -r f310e9eabf60 -r 10a9c31a22b4 doc-src/IsarRef/Thy/Inner_Syntax.thy --- 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 "\"} @{verbatim "''"} \\ + @{syntax_def (inner) str_token} & = & @{verbatim "''"} @{text "\"} @{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). diff -r f310e9eabf60 -r 10a9c31a22b4 doc-src/IsarRef/Thy/document/Inner_Syntax.tex --- 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). diff -r f310e9eabf60 -r 10a9c31a22b4 src/HOL/String.thy --- 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 diff -r f310e9eabf60 -r 10a9c31a22b4 src/HOL/Tools/string_syntax.ML --- 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"}, diff -r f310e9eabf60 -r 10a9c31a22b4 src/Pure/Syntax/lexicon.ML --- 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)); diff -r f310e9eabf60 -r 10a9c31a22b4 src/Pure/Syntax/syntax.ML --- 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"]); diff -r f310e9eabf60 -r 10a9c31a22b4 src/Pure/pure_thy.ML --- 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 _"),