Re: [isabelle] Basic IsarToLatex markup completed

On Fri, 30 Nov 2012, Gottfried Barrow wrote:

Here are three things that would make for safer markup:

1) You leave \<^isub> and \<^isup> in Isar.

2) They and the character that follows them get ignored, other than the fact that the character gets subscripted or superscripted.

Does that mean you want to write "foo\<^sub>\<lless>" as identifier?
Or \<^sub>\<lless> anywhere in the Isar outer syntax to be like a blank?

3) They're highlighted different than the characters following \<^sub> and \<^sup>.

Without item three, it might just end up confusing people, if they're trying to figure out what the markup tags are. Is it \<^isub>' or \<^sub>'? You wouldn't be able to tell.

The confusion of \<^isub> version \<^sub> has been there all the time, starting when \<^isub> was introduced. There were historical reasons to have subscripts within an identifier different from subscripts as part of notation, because there was a built-in notation using it (a variant of application). So there might actually be a chance now to unify identifier syntax to use \<^sub> only, and drop the special rendering of \<^isub> \<^isup> in Isabelle/jEdit.

In general, the jEdit text view can render "\<^foo>\<bar>" or "\<^foo>a" in almost arbitrary ways that fit on a 1-dimensional line of text. Any affine transformation on the font can be applied. For \<^sub>a the glyph for \<^sub> is made very thin (and in the next release also with 100% transparency) and the "a" is scaled/translated to give a nice subscript (nicer than the official Java subscript style).

One could also change the font family on the spot, for each of the two symbols separately, but this is presently not done.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.