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