[isabelle-dev] Deprecating legacy ASCII symbols?

[Makarius]

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