[isabelle-dev] html output of theories

[Christian Sternagel]

On 04/14/2014 12:01 PM, Makarius wrote:
> So what are the characteristic points for theory presentation, either
>
>    (1) as paginated PDF,
>    (2) as static HTML,
>    (3) as dynamic document within the Prover IDE?

I hope I got it right that you are interested in opinions here? 
Otherwise, sorry ;)

(1) I think this is most important for using Isabelle when typesetting a 
paper. At the moment I do either of two things:
   - Use a theory Snippets.thy that just recapitulates some existing 
definitions/lemmas/... and generate latex snippets to be included in my 
paper (mostly when working together with researchers that are not using 
Isabelle themselves). Or
   - use a theory Paper.thy whose corresponding paginated PDF *is* my 
paper.

(2) I mostly use HTML for browsing Isabelle theories. But at the moment 
this is not very comfortable (no links from constants to their 
definition, nor from lemma names to the corresponding lemma, ...). 
However this is all there in Isabelle/jEdit. And my only reason for not 
using Isabelle/jEdit for the above purpose is that I have to wait until 
everything is loaded, whereas somebody else already generated the HTML 
for HOL/Library, AFP, etc. I also agree that HTML output is important 
for people who don't know Isabelle yet.

(3) This is what we all use every day, right? So this should be most 
sophisticated (and already is, I think). Presentation wise the only 
negative point I can think of, is that ugly LaTeX code is mostly 
unreadable in the theory-file, while I need it sometimes for (1). In 
that respect it would be wonderful if either Isabelle/jEdit would 
magically present the result of TeXing or support nicely rendered syntax 
for formatting (I think there is no way around LaTeX when it comes to 
rendering formulas. Maybe there is. Do you know MathML?).

cheers

chris