The Coq mailing list

[Makarius <makarius AT sketis.net>]

On Fri, 26 Feb 2016, Clément Pit--Claudel wrote:

> > Interestingly, that release also parts with official Unicode in various 
> > ways, e.g. see "more arrow symbols" announced here 
> > http://isabelle.in.tum.de/dist/Isabelle2016/doc/NEWS.html.
>
> I don't think this implies departing from Unicode, except to the extent 
> that you're introducing new glyphs. There are simple ways do this while 
> remaining compliant (see http://www.unicode.org/faq/private_use.html). 
>
> > Hopefully you see there arrows of length 3 and 4, taken from a
> > server-side font that is also used in the IDE.
>
> There seems to be a bug in that page. The sources include:
>  <meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
> and further down:
>  Support for more arrow symbols, with rendering in LaTeX and Isabelle fonts: 
> ⇚ ⇛ ⤎ ⤏ ⇠ ⇢.
>
> If the intent is that these should display as long arrows, then 
> charset=utf-8 is incorrect. Instead of using previously unassigned codes 
> for extra arrows, it seems that Isabelle decided instead to recycle 
> existing UTF-8 codes for "(LEFT/RIGHT)WARDS (DOUBLE/TRIPLE) DASH ARROW", 
> thus creating a new coding system (diverging slightly from UTF-8).

This is why I said we are more and more departing from official Unicode -- 
and were actually never really using it. The task is not to comply with a 
monster standard, but to support mathematical symbols in formal texts 
(including sub/superscripts and bold face).

The rendering of ⤎ ⤏ ⇠ ⇢ (officially arrows with 3/4 dashes) as arrows 
of length 3/4 is just one of many workarounds to make something useful out 
of the situation. As long as the Isabelle font is used, it is shown as 
intended. Outside of this context (i.e. copied into some email or onto 
Stackoverflow) it still makes some sense, if the system font happens to 
provide these standard glyphs. It should be clear to users that a text 
terminal or mail reader is not as accurate as the Prover IDE itself (or 
its LaTeX-based document preparation system).


> Is that right? This means that Isabelle sources will look funny if 
> viewed in a git diff, on GitHub

Isabelle users Mercurial, not git. But the question is the same: sources 
are stored without Unicode encoding in clear text, e.g. see 
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2016/NEWS

For the Prover IDE, this representation counts as "encoding", which is 
defined as part of the jEdit plugin. In principle it could be also done 
for the JVM. Thus Isabelle symbols look like normal Unicode strings to JVM 
applications, but they need to be handled with care.


> in emails, and in any other places that do not use Isabelle's custom 
> font. Switching to that font as the system default, on the other hand, 
> will break dashed arrows in every other program.

The principle is this: authentic sources are stored as plain text with 
explicit symbol names.  Thus the repertoire of symbols is easily 
extensible and decodable by archeologists who find our proof repositories 
in distant future.


Mails and adhoc views in editors or browsers are less authentic, using 
Unicode only as a poor-man's rendering tool.

Such rendering can go badly wrong, if official Unicode standards are 
observed, e.g. in the change of left-to-right versus right-to-left 
characters. See the bottom of 
http://isabelle.in.tum.de/dist/library/HOL/HOL-ex/Hebrew.html -- I made 
this example quite enthusiastically, when Unicode was first supported in 
some version of XEmacs, before Emacs 22 started to support Unicode. Only 
much later, I discovered that Emacs was rendering that wrongly: In the 
final lemma, the "He" and the "135" need to be swapped across the equation 
sign. This gives mathematical nonsense, but is correct Unicode text 
rendering. (I should probably explain this explicitly in the example.)

There are more such traps hidden in Unicode, e.g. "Combining Characters". 
This means you can never be quite sure what the equality on character 
strings really is.


The conclusion is that Isabelle does not support official Unicode, but 
uses it as approximative tool to render its infinite collection of named 
symbols. That should be understood as a flat version of LaTeX math, with 
visual representation in the editor.


        Makarius