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