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