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



On Mon, 10 Sep 2012, Gottfried Barrow wrote:

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.

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.


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.

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>.


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.

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.


Just last week I was preparing some slides in Isabelle, and found the traditional latex batch-run quite cumbersome, so the obvious thing is to renovate the HTML presentation instead and make it render on the spot in real-time in Isabelle/jEdit (lets say in some Preview panel).

My main concern at the moment is to find good in-text representation of list environments; bold, emphasize, or even text colors would be obvious extensions. Apart from implementation efforts, an open question is how to spell this out in the source text. Maybe a reduced version of Markdown? But the whole thing needs to be conservative over the embedded LaTeX in Isabelle theories.

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


	Makarius





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