inner syntax positions for string literals;

--- a/src/HOL/String.thy	Mon Nov 14 17:47:59 2011 +0100
+++ b/src/HOL/String.thy	Mon Nov 14 17:48:26 2011 +0100
@@ -69,7 +69,7 @@
   by (simp add: fun_eq_iff split: char.split)
 
 syntax
-  "_Char" :: "xstr => char"    ("CHR _")
+  "_Char" :: "xstr_position => char"    ("CHR _")
 
 
 subsection {* Strings *}
@@ -77,7 +77,7 @@
 type_synonym string = "char list"
 
 syntax
-  "_String" :: "xstr => string"    ("_")
+  "_String" :: "xstr_position => string"    ("_")
 
 use "Tools/string_syntax.ML"
 setup String_Syntax.setup

--- a/src/HOL/Tools/string_syntax.ML	Mon Nov 14 17:47:59 2011 +0100
+++ b/src/HOL/Tools/string_syntax.ML	Mon Nov 14 17:48:26 2011 +0100
@@ -52,6 +52,8 @@
       (case Lexicon.explode_xstr xstr of
         [c] => mk_char c
       | _ => error ("Single character expected: " ^ xstr))
+  | 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);
 
 fun char_ast_tr' [c1, c2] =
@@ -72,6 +74,8 @@
             [Ast.Constant @{syntax_const "_constrain"},
               Ast.Constant @{const_syntax Nil}, Ast.Constant @{type_syntax string}]
       | cs => mk_string cs)
+  | string_ast_tr [Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, ast1, ast2]] =
+      Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, string_ast_tr [ast1], ast2]
   | string_ast_tr asts = raise Ast.AST ("string_tr", asts);
 
 fun list_ast_tr' [args] =

--- a/src/Pure/Syntax/syntax.ML	Mon Nov 14 17:47:59 2011 +0100
+++ b/src/Pure/Syntax/syntax.ML	Mon Nov 14 17:48:26 2011 +0100
@@ -543,7 +543,7 @@
   (Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
     "args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms",
     "any", "prop'", "num_const", "float_const", "index", "struct",
-    "id_position", "longid_position", "type_name", "class_name"]);
+    "id_position", "longid_position", "xstr_position", "type_name", "class_name"]);
 
 
 

--- a/src/Pure/pure_thy.ML	Mon Nov 14 17:47:59 2011 +0100
+++ b/src/Pure/pure_thy.ML	Mon Nov 14 17:48:26 2011 +0100
@@ -135,6 +135,7 @@
     ("_constrainAbs", typ "'a",                        NoSyn),
     ("_position",   typ "id => id_position",           Delimfix "_"),
     ("_position",   typ "longid => longid_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 _"),