On Sat, 13 Jul 2013, Alexander Krauss wrote:
On 07/10/2013 07:25 PM, Makarius wrote:
Even simpler would be to invent a name for some variant of \<omega> that
is not considered a letter, and use that with \<^sup> as before. That
would be analogous to \<epsilon> vs. \<some>.
Does the mapping from Isabelle symbols to Unicode code points have to be
injective? Otherwise, this would be an easy way to escape the problem: Just
have \<omegasym>, which displays as omega, but is not a letter...
Yes, the mapping has to be injective. There happen to be two slightly
different epsilons in the Unicode charts, so these are used here for
\<epsilon> vs. \<some>. (The trick goes far back to X-Symbol with actual
X11 fonts, not unicode at all.)
A second omega is more difficult. Browsing the charts 2-3 more times, I
only see the Mathematical Alphanumeric Symbols (1D400..1D7FF) as
possibility. These provide several copies of everything for "math mode",
in the manner of TeX. They were introduced only recently on request of
the STIX project, and are rarely included in other fonts.
The latter is not so much of a problem, though: our default symbol
assigment usually follows the idea that the standard rendering is via the
IsabellText font and STIX as a fall-back.
I am more worried about the waterbed syndrome: getting rid of a second
copy of sub/sup, but introducing a second copy of greek symbols that are
not letters. That would be actually more correct, but also more
confusion: unicode greeks are for prose text in that language, but
everybody uses them for math as well; having actual math greeks is a bit
too sophisticated to my taste.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
