* 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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
