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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
