[isabelle-dev] html output of theories

[Makarius]

On Sat, 12 Apr 2014, John Wickerson wrote:

> One problem with all this is that the contents of "text {* ... *}" is 
> generally written in LaTeX. It would be desirable if this could also be 
> exported to HTML. Maybe one has to resort to using something like HeVeA?

I am asking myself these questions for a long time.  HeVeA looks like a 
relatively advanced tool for its job.  The deeper question is how much 
LaTeX is there actually in the average Isabelle/Isar proof document.

I've recently started to think about adding a bit of Markdown 
(https://daringfireball.net/projects/markdown) to the 'text' syntax in a 
conservative way, such that there is no LaTeX required for basic things 
like itemize/enumerate/description, and it also looks better in the 
editor.

A general observation is that Isabelle/jEdit has become more and more a 
live document browser, now even with Navigator (e.g. in current 
Isabelle/282f3b06fa86).  So one could also ask the question what is still 
missing to eliminate the need for separate HTML browsing.

So what are the characteric points for theory presentation, either

   (1) as paginated PDF,
   (2) as static HTML,
   (3) as dynamic document within the Prover IDE?


 	Makarius