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



Makarius,

If you get some ideas from this that's good, but I'll do 6 things and then back out of 5 of them.

I don't want to work with LaTeX right now, but I'm switching things around so that I can either build a PDF through Isabelle, or through my own scripts.

I switch to "text{*...*}" to use it like it's typically used, and I use `--"...."` for adding comments to proofs and other syntax.

I get rid of the bullets and make more intelligent use of subsubsection. When everything ends ups having a bullet, they lose their effect.

I use the section commands like normal; I get rid of the bold text in the section title, and I get rid of the duplicate title.

It's worth spending some time to try and format the code so that it's more readable in jEdit, but complexity can only be reduced so much.

Cheap imitations aren't the way to go if they complicate things too much. LaTeX is supposed to extend things, not be duplicated.

Other than \<^bold> in identifiers, you could lock in jEdit today for 2 or 3 years, and it would be good enough.

I see on [isabelle-dev] that it's not locked in, and the speed improvements sound good. If users can create huge theories beyond Complex_Main, and other users can use those theories without having to build the heap, that simplifies things. Speed can solve a lot of problems.

Regards,
GB



On 9/21/2012 1:15 PM, Makarius wrote:
On Mon, 17 Sep 2012, Gottfried Barrow wrote:

As to why I use --"......" instead of "text{*....*}", (*....*), and --{*...*}, that gets into the analysis of what I'm trying to accomplish in my first phase of editing a THY file. I'm always happy to analyze things.

My source code editing method could partially described with these phrases: "readability", "absorb information fast", "get around fast", "don't let the code get so unwieldy you don't know what's there", and "always have an idea of where you're at in the code on an outline level".

Some of these aspects are shared by projects like Markdown, which I have encountered just recently myself, although the ideas (and tools) are already there for several years. The idea is to write plain text with some level of "formality", such that the immediately readable text can be typeset in reasonable quality offline (or as preview online, like in the "enki" editor).

I've started thinking about making Isabelle section / text / "--" follow some Markdown principles. You have already \<bullet> symbols that approximate a formal itemization. A bit more such things could become standard one day.


Here's where someone might think I would make a request of you. I could request that you hide the syntax "section{*", and based on command context, make the words inside "section{*.....*}" bold.

Maybe in the next round of jEdit trickery. There is still the TokenMarker limitation imposed by the original code base, but I might eventually manage to get a tiny little modification accepted by the jEdit maintainers to make font styles dependent on a semantic context, not just the plain text you see in the buffer.


I'm still experimenting. For example, the blue and boldfaced keyword "theorem" is not enough to make it stand out from lots of other keywords in its vicinity. I'm currently experimenting with this for unnamed theorems, like this:

theorem --"\<^bold>(*\<^bold>) What the theorem does starts here..."

With that, I can also replace "*" with a number, if needed, so that I can reference it within a section.

BTW, there is a semiformal "tag" concept that could be used here:

  theorem %important ...

Right now these tags are mainly relevant for LaTeX output, but one could make more of them. You can also try to be creative with non-alphabetic tag names, although LaTeX will choke on that.


I'm still looking for a more perfect symbol than "*". \<bullet> is not vertically centered in the "( )", and "*" doesn't stand out enough.

It seems that when merging Bitstream Vera and TeX fonts in IsabelleText, I've got the spacing not exactly right. This is the normal situation for a non-fontdesigner like myself tinkering with existing fonts. Nonetheless the outcome is so much better than anything we've had in the last 15 years, and also slightly better than STIX in many respects.


I try things like \<^bold>(\<^bold>\<^bold>). I need to identify theorems quick when they're interspersed with a bunch of bulleted text. But now, I'm in realm of "personal tweaking".

Personal tweaking may be perfected by assigning your own (unused) Unicode points to (unused) Isabelle symbols in $ISABELLE_HOME_USER/etc/symbols like this:

  \<blob>   code: 0x2593 font: STIXGeneral

This gives you a 75% grey shade quad, assuming you and your recipients have that font and your etc/symbols file. Otherwhise they will see a literal \<blob> which is also OK.


Both "text{*....*}" and --"....." make the background grey, and I would turn that off if I could. An example of "I live with it", because it's not a problem. The grey is a little too dark on my laptop monitor, but I mainly have jEdit on my external monitor.

In the next Isabelle release, all these colors will be configurable via user options. Then people can come up with their own "themes".


    Makarius








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