Re: [isabelle] unicode tokens in isabelle2011+pg4.0

On Wed, 2 Feb 2011, Alexander Krauss wrote:

Are you saying that the Unicode code points listed in $ISABELLE_HOME/etc/symbols may not occur regularly in the sources? The section in the implementation manual does not make this clear... In fact what I read there is that any UTF-8 sequence is legal. So then it should not be a problem to declare the ab

Or is it an additional constraint imposed by the jEdit layer? PG 4 seems to differentiate between the different classes of symbols...

Isabelle symbols co-exist with arbitrary UTF-8 sequences. The encoding back and forth for "poor-man's rendering" in the front-end is a slightly different thing. It is not injective, so overlap needs to be avoided.

Also note that $ISABELLE_HOME/etc/symbols is just one default table. Users may have there own.

When struggling with this unicode mess over the 1-2 years, I could not imagine that anybody could actualy love unicode. In the next round I will try harder produce explicit errors on bad sources.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.