On 9/12/2012 3:30 PM, Makarius wrote:
I think it is better to move in a presentational direction: you write the formal text without special markup for italics, but the implicit markup as logical identifiers that the prover provides is turned into italics on-screen. So it would be just a continuation of the blue, green, brown variable game with font-styles.
It did occur to me that when "every character" is italicized, I really don't want to be putting an \<italic> in front of "every character". Trying to back out of that could end up being a nightmare, or really aggravate someone else wanting to use my stuff.
It sounds like plans for even more of a Mathematica thing.
I did not do this so far, because jEdit cannot change the font-style once it has been assigned statically by its token marker. It will require another round of convincing it to do it nonetheless -- like I already did with the text rendering as you see it in Isabelle2012.
Actually, with Mathematica, their document model is way more complex than what I need, or have time to learn.
A combination of basic text editing, with an 80 character column, a few extra symbols, some consistent formatting using your comment command `--"........"`, and section headings, are good enough to make things readable. The math formulas are pretty much readable by default.
With Isabelle2011, I was using LaTeX to produce a readable document. Recently, I broke my LaTeX build script, and before I got it fixed, I said, "Forget LaTeX right now. I have 500 pages of theorems I have to implement, and if I can't make it all work, then it's worthless to make something look good that's worthless."
I attach a screen shot. How would it print out with LaTeX? It would look terrible, I'm sure, but that's not the purpose. If I want to print it, I can print it out with a regular printer driver. But I read everything in electronic form, so I always need a tree view, and Sidekick gives me that in jEdit.
Description: PNG image