[isabelle-dev] string and altstring

[Christian Sternagel]

Dear all,

currently it is possible to write something like "\"" , "\\", `\``, or 
`\\` (i.e., there are escape sequences for the delimiters of strings and 
altstrings, as well as for backslash).

What many people might be used to from programming languages does not 
work however, e.g., "\n", "\t", ...

For that reason we currently have some abbreviations like the following 
in IsaFoR:

   abbreviation tab :: "char" where
     "tab ≡ Char Nibble0 Nibble9"
   abbreviation newline :: char where
     "newline ≡ Char Nibble0 NibbleA"
   abbreviation carriage_return :: "char" where
     "carriage_return ≡ Char Nibble0 NibbleD"
   abbreviation wspace :: "char list" where
     "wspace ≡ CHR '' '' # newline # tab # carriage_return # []"

(Maybe there is a better solution?)

Would it make sense to allow the most common escape sequences (like 
"\n", "\t", "\r", etc.)? Then I could use

   CHR ''\t'', CHR ''\n'', CHR ''\r'', '' \n\t\r''

instead of the above.

Btw: Why does "CHR ''\013''" result in "Char Nibble0 NibbleA"? Shouldn't 
that be "Char Nibble0 NibbleD"?

cheers

chris