Email Gateway (Aug 19 2022 at 11:39): Email Gateway (Aug 19 2022 at 11:39):From: Makarius <makarius@sketis.net>
This is off-topic on isabelle-dev ...
The syntax for quoted material in Isabelle deviates in various fine points
from what you see in some other languages, but there were various reasons
to arrive there over many years. I can't recall all of them on the spot.
Any change will inevitably break many things and require years to sort it
out. So as usual there need to be 2-3 really good reasons to consider
that at all.
The standard way to get a line-feed into the HOL term language is indeed
term "CHR ''\010''". It is funny that "CHR ''\013''" also normalizes to
the same -- there are a few more such normalizations built into the notion
of Isabelle symbols, which underlies all text that the prover processes.
Generally, when working with text, especially on top of unicode, there can
be a number of really big surprises. Isabelle avoids most of the dangers
of official Unicode by working with its symbols instead, but this is not
100% bullet proof. We are living in a time where computer systems cannot
process text material reliably and unambigously ...
Makarius
Last updated: Apr 26 2024 at 01:06 UTC