inner syntax positions for string literals;
authorwenzelm
Mon Nov 14 17:48:26 2011 +0100 (2011-11-14)
changeset 4549020c8c0cca555
parent 45489 9b6f55f34b70
child 45491 3c9aff74fb58
child 45494 e828ccc5c110
inner syntax positions for string literals;
src/HOL/String.thy
src/HOL/Tools/string_syntax.ML
src/Pure/Syntax/syntax.ML
src/Pure/pure_thy.ML
     1.1 --- a/src/HOL/String.thy	Mon Nov 14 17:47:59 2011 +0100
     1.2 +++ b/src/HOL/String.thy	Mon Nov 14 17:48:26 2011 +0100
     1.3 @@ -69,7 +69,7 @@
     1.4    by (simp add: fun_eq_iff split: char.split)
     1.5  
     1.6  syntax
     1.7 -  "_Char" :: "xstr => char"    ("CHR _")
     1.8 +  "_Char" :: "xstr_position => char"    ("CHR _")
     1.9  
    1.10  
    1.11  subsection {* Strings *}
    1.12 @@ -77,7 +77,7 @@
    1.13  type_synonym string = "char list"
    1.14  
    1.15  syntax
    1.16 -  "_String" :: "xstr => string"    ("_")
    1.17 +  "_String" :: "xstr_position => string"    ("_")
    1.18  
    1.19  use "Tools/string_syntax.ML"
    1.20  setup String_Syntax.setup
     2.1 --- a/src/HOL/Tools/string_syntax.ML	Mon Nov 14 17:47:59 2011 +0100
     2.2 +++ b/src/HOL/Tools/string_syntax.ML	Mon Nov 14 17:48:26 2011 +0100
     2.3 @@ -52,6 +52,8 @@
     2.4        (case Lexicon.explode_xstr xstr of
     2.5          [c] => mk_char c
     2.6        | _ => error ("Single character expected: " ^ xstr))
     2.7 +  | char_ast_tr [Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, ast1, ast2]] =
     2.8 +      Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, char_ast_tr [ast1], ast2]
     2.9    | char_ast_tr asts = raise Ast.AST ("char_ast_tr", asts);
    2.10  
    2.11  fun char_ast_tr' [c1, c2] =
    2.12 @@ -72,6 +74,8 @@
    2.13              [Ast.Constant @{syntax_const "_constrain"},
    2.14                Ast.Constant @{const_syntax Nil}, Ast.Constant @{type_syntax string}]
    2.15        | cs => mk_string cs)
    2.16 +  | string_ast_tr [Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, ast1, ast2]] =
    2.17 +      Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, string_ast_tr [ast1], ast2]
    2.18    | string_ast_tr asts = raise Ast.AST ("string_tr", asts);
    2.19  
    2.20  fun list_ast_tr' [args] =
     3.1 --- a/src/Pure/Syntax/syntax.ML	Mon Nov 14 17:47:59 2011 +0100
     3.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Nov 14 17:48:26 2011 +0100
     3.3 @@ -543,7 +543,7 @@
     3.4    (Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
     3.5      "args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms",
     3.6      "any", "prop'", "num_const", "float_const", "index", "struct",
     3.7 -    "id_position", "longid_position", "type_name", "class_name"]);
     3.8 +    "id_position", "longid_position", "xstr_position", "type_name", "class_name"]);
     3.9  
    3.10  
    3.11  
     4.1 --- a/src/Pure/pure_thy.ML	Mon Nov 14 17:47:59 2011 +0100
     4.2 +++ b/src/Pure/pure_thy.ML	Mon Nov 14 17:48:26 2011 +0100
     4.3 @@ -135,6 +135,7 @@
     4.4      ("_constrainAbs", typ "'a",                        NoSyn),
     4.5      ("_position",   typ "id => id_position",           Delimfix "_"),
     4.6      ("_position",   typ "longid => longid_position",   Delimfix "_"),
     4.7 +    ("_position",   typ "xstr => xstr_position",   Delimfix "_"),
     4.8      ("_type_constraint_", typ "'a",                    NoSyn),
     4.9      ("_context_const", typ "id_position => logic",     Delimfix "CONST _"),
    4.10      ("_context_const", typ "id_position => aprop",     Delimfix "CONST _"),