[isabelle-dev] Subscripts within identifiers
makarius at sketis.net
Wed Jul 10 19:25:46 CEST 2013
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>.
More information about the isabelle-dev