[isabelle-dev] Subscripts within identifiers

[Makarius]

On Wed, 10 Jul 2013, Tobias Nipkow wrote:

> Am 10/07/2013 16:54, schrieb Makarius:
>> That is an instance of \<^sup>LETTER, i.e. the remaining overlap from the
>> earlier discussion on this thread.  I have presently escaped the situation by
>> using \<^bsup> \<^esup> which looks almost the same in Latex, but is a bit
>> awkward in Isabelle/jEdit.
>
> Why don't you display \<^bsup> \<^esup> properly in jedit, then the 
> problem is reduced?

That is not so easy to implement, and it just did not have this priority 
to justify spending time on it so far or in the near future.

Conceptually, the stream of Isabelle symbols does not have any block 
structure, neither has the editor's tokenenization mechanism, so it is 
better not to pretend that it is different. (PG / Emacs was choking a lot 
on these quasi block controls in the past, and there are still bad 
situations left; I don't want to recall the old things.)

A much simpler approach (in conformance with the Isabelle symbols idea) 
would make \<omegasuperior> a "predefined" Isabelle symbol with a suitable 
glyph to the font and latex macro.

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


 	Makarius