[isabelle-dev] Subscripts within identifiers

[Makarius]

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