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

On 9/12/2012 1:43 PM, Makarius wrote:

From the other email of yours:
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).
From this email:
In formal text italic style does not make much sense, because the formal text is implicitly "italic" already. You see this when printing in LaTeX in the "best style" \isabellestyle{it} that imiates Don Knuth as best as possible. If you need "non-italic" special styles, you can define your own symbols like \<sin> \<cos> \<tan> and render them in LaTeX as usual. In informal text, one could think of bold and italic in the sense of Markdown. What is a good notation for that? It needs to co-exist with regular latex macros.

Markarius, I'm not using your tool the same way you use it.

To summarize, what I'm trying to get even more is a "logical Mathematica thing". Ultimately, I don't have to have \<iitalic> and \<ibold>, my use of jEdit as a "Mathematica thing" is already happening.

I quoted from the last email because that applies, although not the "preview", though that sounds like a good thing. I want to write like I'm writing in a word processor, and that's what I'm already doing.

My marked up THY file is what I'll call a pre-LaTeX version. LaTeX is compile, compile, compile, and compile after every few changes to prevent having to track down errors. Plus, I'll spend an hour trying to make an equation look perfect, when all I'm doing is making notes about a textbook. That's a waste when I may delete much of what I do.

There will be what I publish for public consumption, which will be a LaTeX product, but my preliminary markup of a THY file is for me. I need to not get lost in the details, which is a combination of markup using bullets and other symbols, using section headings with bold titles, and Sidekick trees.

So \<^iitalic> is not a duplication of effort when a person is primarily reading a theory with jEdit, rather than a PDF. Would I want to italicize every variable in a formula? I might. I can already subscript and superscript every variable, and put things like "\<^isub>_" in them.

I can get LaTeX without your LaTeX tools, but I can only get in jEdit what you provide in jEdit. But what you've given is very generous.


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