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



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

\<^ibold>,

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.

Regards,
GB

On 9/10/2012 12:00 PM, Gottfried Barrow wrote:
Hi,

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.

Regards,
GB








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