[isabelle-dev] NEWS: newline in HOL char or string literals

[Makarius]

* The symbol "\<newline>" may be used within char or string literals
to represent (Char Nibble0 NibbleA), i.e. ASCII newline.

This refers to Isabelle/e33c5bd729ff, which also introduces a unicode 
glyph for that.

It is a continuation of the isabelle-users thread: 
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2013-August/004457.html 
by Christian Sternagel.


As usual there is the difference of what one wants vs. needs vs. can have. 
The \<newline> symbol is easy to have, and it is sufficient for the 
applications in IsaForR, after studying the sources a bit.  So that is 
needed here.

Classic C notation \n is not easy to have, and not needed.

Tab \t and CR \r were mentioned in the old thread as well.  These are evil 
characters, but they might occur in some formal model in HOL nonetheless. 
I did not find any convenient unicode glyphs, though.  Moreover, Isabelle 
symbols cannot distinguish \n vs. \r vs. \r\n, otherwise Windows files 
cannot be processed properly; jEdit incidently does the very same collapse 
of line endings.

So in exotic applications of HOL where strange whitespace characters are 
needed, explicit (Char NibbleX NibbleY) will do the job as before.


 	Makarius