[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:
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