# HG changeset patch
# User haftmann
# Date 1524647065 0
# Node ID ad4b8b6892c3f460cd9e6f73a5211fd6852e1f2f
# Parent  412fe0623c5d1619ef44ccbb17d293ea2a8ba58f
uniform tagging for printable and non-printable literals

diff -r 412fe0623c5d -r ad4b8b6892c3 NEWS
--- a/NEWS	Tue Apr 24 22:22:25 2018 +0100
+++ b/NEWS	Wed Apr 25 09:04:25 2018 +0000
@@ -210,7 +210,7 @@
   * Type "String.literal" (for code generation) is now isomorphic
     to lists of 7-bit (ASCII) values; concrete values can be written
     as "STR ''...''" for sequences of printable characters and
-    "ASCII 0x..." for one single ASCII code point given
+    "STR 0x..." for one single ASCII code point given
     as hexadecimal numeral.
 
   * Type "String.literal" supports concatenation "... + ..."
diff -r 412fe0623c5d -r ad4b8b6892c3 src/Doc/Codegen/Adaptation.thy
--- a/src/Doc/Codegen/Adaptation.thy	Tue Apr 24 22:22:25 2018 +0100
+++ b/src/Doc/Codegen/Adaptation.thy	Wed Apr 25 09:04:25 2018 +0000
@@ -174,7 +174,7 @@
 
        Literal values of type @{typ String.literal} can be written
        as @{text "STR ''\<dots>''"} for sequences of printable characters and
-       @{text "ASCII 0x\<dots>"} for one single ASCII code point given
+       @{text "STR 0x\<dots>"} for one single ASCII code point given
        as hexadecimal numeral; @{typ String.literal} supports concatenation
        @{text "\<dots> + \<dots>"} for all standard target languages.
 
diff -r 412fe0623c5d -r ad4b8b6892c3 src/HOL/Library/Code_Test.thy
--- a/src/HOL/Library/Code_Test.thy	Tue Apr 24 22:22:25 2018 +0100
+++ b/src/HOL/Library/Code_Test.thy	Wed Apr 25 09:04:25 2018 +0000
@@ -84,8 +84,8 @@
 
 definition list where "list f xs = map (node \<circ> f) xs"
 
-definition X :: yxml_of_term where "X = yot_literal (ASCII 0x05)"
-definition Y :: yxml_of_term where "Y = yot_literal (ASCII 0x06)"
+definition X :: yxml_of_term where "X = yot_literal (STR 0x05)"
+definition Y :: yxml_of_term where "Y = yot_literal (STR 0x06)"
 definition XY :: yxml_of_term where "XY = yot_append X Y"
 definition XYX :: yxml_of_term where "XYX = yot_append XY X"
 
diff -r 412fe0623c5d -r ad4b8b6892c3 src/HOL/String.thy
--- a/src/HOL/String.thy	Tue Apr 24 22:22:25 2018 +0100
+++ b/src/HOL/String.thy	Wed Apr 25 09:04:25 2018 +0000
@@ -119,7 +119,7 @@
 lemma char_of_nat [simp]:
   "char_of (of_nat n) = char_of n"
   by (simp add: char_of_def String.char_of_def drop_bit_of_nat)
-	
+
 end
 
 lemma inj_on_char_of_nat [simp]:
@@ -407,7 +407,7 @@
 
   \<^enum> Printable text as string prefixed with @{text STR};
 
-  \<^enum> A single ascii value as numerical value prefixed with @{text ASCII}.
+  \<^enum> A single ascii value as numerical hexadecimal value prefixed with @{text STR}.
 \<close>
 
 instantiation String.literal :: zero
@@ -455,8 +455,8 @@
 code_datatype "0 :: String.literal" String.Literal
 
 syntax
-  "_Ascii" :: "num_const \<Rightarrow> String.literal"        ("ASCII _")
   "_Literal" :: "str_position \<Rightarrow> String.literal"   ("STR _")
+  "_Ascii" :: "num_const \<Rightarrow> String.literal"        ("STR _")
 
 ML_file "Tools/literal.ML"