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

On Thu, 13 Sep 2012, Gottfried Barrow wrote:

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've recently seen myself doing "drafting" directly in the editor buffer, with its slightly improved rendering quality in the last 12 months or so. The jEdit print operation also produces suprisingly good results with the IsabelleText font.

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.

The LaTeX appearance is defined by the .sty files you provide to render it. The default isabelle.sty would make inlined comments with "--" look unsatisfactory, for example. Normally you use the 'text' command for larger paragraphs of semi-formal text.

What is the purpose of the paragraph signs in your source (in the 'section' command)?


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