[isabelle-dev] html output of theories

[John Wickerson]

Hi Makarius,

> 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.

I think separate HTML browsing is very important, and should not be eliminated. I can think of three instances where it is very helpful.

[Attracting new Isabelle users.] Alice is browsing the web, stumbles upon MyIsabelleTheory.html, finds it impressively readable (what with all the properly-formatted "text{*...*}" blocks, the hyperlinked structure, the self-documenting tooltips, the syntax highlighting, etc), and wants to download Isabelle herself. Even with new features for improved usability and document browsing, Isabelle/jEdit can't compete with the web-browser for user familiarity.

[Sharing Isabelle theories with non-Isabellers.] Bob is "the guy who knows Isabelle" on the research team, so he formalises the new proof system that the other researchers come up with. He can't expect the other researchers to download Isabelle/jEdit, so he sends them a link to the .html pages that they can read, to see what he's been up to.

[Viewing the result of antiquotations, and so on.] After typing out lots of antiquotations and so on inside my "text{*...*}" and "header{*...*}" blocks, I would like to see what these will look like in the finished product. I don't want to print it out, so I have no interest in a boring monochrome paginated PDF -- I just want my theory to look like it does in Isabelle/jEdit, but with the antiquotations properly rendered. And I think HTML is probably the right tool for that.

Best wishes,
John