[isabelle] Isar feature request: bbold and ebold


For subscripts I never use \<^bsub> and \<^esub>. They don't work on Cygwin anyway, and I'm too lazy to fire up the VirtualBox Linux to find out if that's true in Linux.

It actually turns out for the better, because subscripting more than two letters is to be minimized, which means I only normally use two \<...> commands anyway, plus \<^isub> works everywhere, and "-_" is easier to type.

However, I am now using \<^bold> in the notes of my comments, or in section headings. To move fast, I'm writing notes using the Isar \<...> symbols to get some better formatting in jEdit, which make my notes more readable for me.

Consider this heading:

section{*\<paragraph> T\<^bold>h\<^bold>e \<^bold>A\<^bold>x\<^bold>i\<^bold>o\<^bold>m \<^bold>o\<^bold>f \<^bold>E\<^bold>x\<^bold>t\<^bold>e\<^bold>n\<^bold>s\<^bold>i\<^bold>o\<^bold>n \<paragraph>*}

That says, "The Axiom of Extension". The bold makes it stand out when I'm scrolling down through a THY, but the additional characters make it hard to read in the Sidekick panel.

At this very moment, I have a bulleted list, and I would like the first phrase of my bulleted item to be bold. To do that, I have to go into my other editor, go to the line, highlight the text, and use a script to put a \<^bold> in front of every letter.

It's just an idea, this \<^bbold> and \<^ebold>. Wants are insatiable. Editors which already have lots of features are very tolerable.


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