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
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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and