[isabelle-dev] html output of theories

[Lawrence Paulson]

PIDE does an awful lot already, and I’d worry about burdening it with yet more functions. 

It’s easy to get PDF from HTML, provided the quality is high enough. The other direction does not work.

Larry

On 15 Apr 2014, at 09:51, Christian Sternagel <c.sternagel at gmail.com> wrote:

> 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev