Re: [isabelle] Isar feature request: bbold and ebold



On 9/12/2012 1:34 PM, Makarius wrote:
What exactly means "don't work" here? In Isabelle/jEdit these control symbols should be shown uniformly as diagonal arrows, without any attempt to make any sub- or superscripting.

Markarius,

So it works after  all. That's what it's doing.

BTW, there is also C-e DOWN. Next time I will make that operate on the text selection as well, for convient superscripting of text ranges, without the conceptual problems of \<^bsub> and \<^esub>.

Thanks for the tip.

Actually, the Isabelle symbols where never meant to be used in informal text, only in formal one. Normally you do document markup in LaTeX, where you would use \textbf{...} as usual. This does not mean there could not be any reforms, but how long it will take is unspecified.

So in that case, I appeal to formal use only, such as \<^ibold> to signify that a variable is a vector. We all know how we'd be in a world of hurt without vectors, and how a vector is represented either with an overhead arrow, or with bold.

I say more about LaTeX markup vs. jEdit markup in the other reply.

Ultimately, jEdit is a simple texteditor, so questions remain how far it can be stretched without breaking down.

I reduce my requests. The commands \<^iitalic> and \<^ibold>, that's all I'm asking for now. I address the italic issue in the other reply.

Regards,
GB





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