The Coq mailing list

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

On 02/26/2016 05:53 PM, Makarius wrote:
> 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).

Aren't subscripts and superscripts a markup issue? They seem to have little 
to do with Unicode.

> 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.

Thanks for the clarification. Is this approach superior to just using a 
smarter display layer, like Emacs does with prettify-symbols-mode or Proof 
General's unicode-tokens (which supported HOL and Isar a while ago)? It seems 
that the core Isabelle is essentially ASCII only, but the IDE comes with a 
rendering engine that uses a translation to and from a non-ASCII string to 
display pretty math into a basic text box. Is this better than using a 
smarter text box (one that would be aware of Isabelle's markup)?

> 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.

I see; thanks. Most Coq developments seem to follow this principle too, using 
plain text only. It's easy then to set up one's editor to display plain text 
documents with pretty symbols (Proof General does it optionally with 
unicode-tokens; company-coq does it by default). If I understand correctly, 
though, Prof. Pierce doesn't seem fully satisfied with this solution.

> 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.

Unicode defines various level of language-awareness in string comparisons, 
all under the headline of collation (http://www.unicode.org/collation/). Is 
this relevant to that issue?

Clément.

Attachment: signature.asc
Description: OpenPGP digital signature