On Tue, 30 Jun 2015, Lars Noschinski wrote:
In the editor buffer in Isabelle/jEdit, everything is mapped to unicode,
so this is no longer an issue.
You are right at a certain level of abstraction, but there is also a
different thread by Lars Hupel about Unicode that I did not answer yet.
The principle we have in Isabelle today is this:
* Isabelle symbols are a plain ASCII notation for infinitely many
mathematical (or other) characters, as specified in the
"implementation" manual.
* Unicode 3.x and a derivate of UTF-8 encoding is used to render that in
the front-end.
This works to the extent that most people think it is all perfect (which
is not the case, because anything involving Unicode cannot be perfect).
But the margin of error is sufficiently small to challange old ASCII
replacement syntax now.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
