Re: [isabelle] Isar feature request: bbold ... (& italics, ibold)

On Tue, 11 Sep 2012, Gottfried Barrow wrote:

I might as well attach related requests, which would be a request for a set of italic commands, like:

\<^iitalic>, \<^bitalic>, and \<^eitalic>,

where \<^iitalic> would be a command that could be used in an identitifer, like \<^isub> and \<^isup>.

And I might as well request


for things like vectors and special sets.

I'm sure Makarius has already thought of all this, and either doesn't have time to do it, or has already decided he doesn't want to do it, maybe because it can't be practically done.

Implementing, maintaining, discontinuing features is all very time consuming -- with increasing efforts on this scale. The \<^sub> \<^isub> \<^bsub> \<^esub> varieties emerged in historic sitations. Even now it should be possible to get there with \<^sub> alone in most applications, but it needs work to untangle all that.

In formal text italic style does not make much sense, because the formal text is implicitly "italic" already. You see this when printing in LaTeX in the "best style" \isabellestyle{it} that imiates Don Knuth as best as possible. If you need "non-italic" special styles, you can define your own symbols like \<sin> \<cos> \<tan> and render them in LaTeX as usual.

In informal text, one could think of bold and italic in the sense of Markdown. What is a good notation for that? It needs to co-exist with regular latex macros.


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