uniform tagging for printable and non-printable literals
authorhaftmann
Wed Apr 25 09:04:25 2018 +0000 (13 months ago)
changeset 68033ad4b8b6892c3
parent 68032 412fe0623c5d
child 68034 27ba50c79328
uniform tagging for printable and non-printable literals
NEWS
src/Doc/Codegen/Adaptation.thy
src/HOL/Library/Code_Test.thy
src/HOL/String.thy
     1.1 --- a/NEWS	Tue Apr 24 22:22:25 2018 +0100
     1.2 +++ b/NEWS	Wed Apr 25 09:04:25 2018 +0000
     1.3 @@ -210,7 +210,7 @@
     1.4    * Type "String.literal" (for code generation) is now isomorphic
     1.5      to lists of 7-bit (ASCII) values; concrete values can be written
     1.6      as "STR ''...''" for sequences of printable characters and
     1.7 -    "ASCII 0x..." for one single ASCII code point given
     1.8 +    "STR 0x..." for one single ASCII code point given
     1.9      as hexadecimal numeral.
    1.10  
    1.11    * Type "String.literal" supports concatenation "... + ..."
     2.1 --- a/src/Doc/Codegen/Adaptation.thy	Tue Apr 24 22:22:25 2018 +0100
     2.2 +++ b/src/Doc/Codegen/Adaptation.thy	Wed Apr 25 09:04:25 2018 +0000
     2.3 @@ -174,7 +174,7 @@
     2.4  
     2.5         Literal values of type @{typ String.literal} can be written
     2.6         as @{text "STR ''\<dots>''"} for sequences of printable characters and
     2.7 -       @{text "ASCII 0x\<dots>"} for one single ASCII code point given
     2.8 +       @{text "STR 0x\<dots>"} for one single ASCII code point given
     2.9         as hexadecimal numeral; @{typ String.literal} supports concatenation
    2.10         @{text "\<dots> + \<dots>"} for all standard target languages.
    2.11  
     3.1 --- a/src/HOL/Library/Code_Test.thy	Tue Apr 24 22:22:25 2018 +0100
     3.2 +++ b/src/HOL/Library/Code_Test.thy	Wed Apr 25 09:04:25 2018 +0000
     3.3 @@ -84,8 +84,8 @@
     3.4  
     3.5  definition list where "list f xs = map (node \<circ> f) xs"
     3.6  
     3.7 -definition X :: yxml_of_term where "X = yot_literal (ASCII 0x05)"
     3.8 -definition Y :: yxml_of_term where "Y = yot_literal (ASCII 0x06)"
     3.9 +definition X :: yxml_of_term where "X = yot_literal (STR 0x05)"
    3.10 +definition Y :: yxml_of_term where "Y = yot_literal (STR 0x06)"
    3.11  definition XY :: yxml_of_term where "XY = yot_append X Y"
    3.12  definition XYX :: yxml_of_term where "XYX = yot_append XY X"
    3.13  
     4.1 --- a/src/HOL/String.thy	Tue Apr 24 22:22:25 2018 +0100
     4.2 +++ b/src/HOL/String.thy	Wed Apr 25 09:04:25 2018 +0000
     4.3 @@ -119,7 +119,7 @@
     4.4  lemma char_of_nat [simp]:
     4.5    "char_of (of_nat n) = char_of n"
     4.6    by (simp add: char_of_def String.char_of_def drop_bit_of_nat)
     4.7 -	
     4.8 +
     4.9  end
    4.10  
    4.11  lemma inj_on_char_of_nat [simp]:
    4.12 @@ -407,7 +407,7 @@
    4.13  
    4.14    \<^enum> Printable text as string prefixed with @{text STR};
    4.15  
    4.16 -  \<^enum> A single ascii value as numerical value prefixed with @{text ASCII}.
    4.17 +  \<^enum> A single ascii value as numerical hexadecimal value prefixed with @{text STR}.
    4.18  \<close>
    4.19  
    4.20  instantiation String.literal :: zero
    4.21 @@ -455,8 +455,8 @@
    4.22  code_datatype "0 :: String.literal" String.Literal
    4.23  
    4.24  syntax
    4.25 -  "_Ascii" :: "num_const \<Rightarrow> String.literal"        ("ASCII _")
    4.26    "_Literal" :: "str_position \<Rightarrow> String.literal"   ("STR _")
    4.27 +  "_Ascii" :: "num_const \<Rightarrow> String.literal"        ("STR _")
    4.28  
    4.29  ML_file "Tools/literal.ML"
    4.30