Re: [isabelle] Isar feature request: bbold ... (& italics, ibold)
On Wed, 12 Sep 2012, Gottfried Barrow wrote:
So \<^iitalic> is not a duplication of effort when a person is primarily
reading a theory with jEdit, rather than a PDF. Would I want to
italicize every variable in a formula? I might. I can already subscript
and superscript every variable, and put things like "\<^isub>_" in them.
I think it is better to move in a presentational direction: you write the
formal text without special markup for italics, but the implicit markup as
logical identifiers that the prover provides is turned into italics
on-screen. So it would be just a continuation of the blue, green, brown
variable game with font-styles.
I did not do this so far, because jEdit cannot change the font-style once
it has been assigned statically by its token marker. It will require
another round of convincing it to do it nonetheless -- like I already did
with the text rendering as you see it in Isabelle2012.
This archive was generated by a fusion of
Pipermail (Mailman edition) and