The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

On 02/26/2016 01:16 PM, Makarius wrote:
> About 8 years ago, I set out to make mathematical symbols "just work"
> for the forthcoming Prover IDE of Isabelle -- uniformly on all 
> platforms. It required several years to get there, and every year I 
> learned new aspects of Unicode that I could not imagine before. In 
> the current release of Isabelle2016 (February 2016) this is mostly 
> routine, and we have again eliminated a lot of old ASCII replacement
>  syntax. 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). This page says

    Private-use characters are code points whose interpretation is not
    specified by a character encoding standard and whose use and
    interpretation may be determined by private agreement among
    cooperating users. Private-use characters are sometimes also referred
    to as user-defined characters (UDC) or vendor-defined characters
    (VDC).

> 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). Is that right? This means that 
Isabelle sources will look funny if viewed in a git diff, on GitHub, 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.

> Note that in standard Unicode fonts, length 2 arrows can already be a
> problem

I don't think this is a Unicode issue. It has to do with whether the user has 
installed a font containing long arrows ( ⟶ and ⟵ ). Such fonts are getting 
more common, but indeed they aren't available everywhere yet. Installing a 
good font is an easy way to solve this issue, and this can happen when 
Isabelle is installed (it already happens for Isabelle's own font).

> and lead to disappointing white or black boxes.

That problem still exists in Isabelle 2016; see 
https://i.imgur.com/KoibYJu.png. In fact, it seems that Isabelle's 
configuration of jEdit ignores other installed fonts, even though they 
contain the right characters. This is visible both when using symbols that 
Isabelle's font do not include, and when writing in non-English scripts, such 
as east Asian scripts; these characters are shown as squares in jEdit, but 
they display properly in my web browser and in most other applications on my 
system.

Cheers,
Clément.

Attachment: signature.asc
Description: OpenPGP digital signature