[isabelle-dev] html output of theories

[John Wickerson]

Hi all,

I've been thinking about and playing with the "theory to HTML" feature of Isabelle. The PDF output is handy for producing papers, but I do find HTML so much easier to read onscreen than PDFs. I mostly use Isabelle/jEdit for browsing theories, but I think HTML output is still very important, e.g. so that people who don't have Isabelle installed can still read my theories.

Here is a little attempt at a prototype of what "Option.thy" might look like after being exported to HTML.

> https://dl.dropboxusercontent.com/u/26024007/isabelle/Option.html


For comparison, here is the original:

> http://isabelle.in.tum.de/library/HOL/HOL/Option.html


And here is the PDF output (not very readable onscreen, and not interactive):

> http://isabelle.in.tum.de/library/HOL/HOL/document.pdf (page 357)

Here is a list of some of the things I've tried to do in this prototype:

1. Interpret "text" and "header" commands so that they "break out" of the Isabelle source. This is like what happens in the PDF output. The current browser_info doesn't do this.

2. More syntax highlighting, like in Isabelle/jEdit. I only bothered to do this for the first couple of lemmas. The current browser_info doesn't have much syntax highlighting.

3. Hyperlinks, like in Isabelle/jEdit. If you hover your mouse over "imports Datatype", you'll see there's a link to "Datatype.html". Same if you hover over the "induct" method. Not that these links currently work, of course.

4. Abolishing double-quotes. I don't think they're necessary for presentation, and they often confuse Isabelle newbies anyway. Instead, I've tried to make *all* of Isabelle's inner-syntax formatted in a uniform way (namely, shaded in a slightly darker grey).

5. More symbols rendered properly. The current browser_info doesn't produce a proper "rightharpoonup" symbol; my new prototype produces the right unicode symbol for this.

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?

By the way, I don't think I have the time or expertise to make much progress on this beyond this little prototype. I just wanted to start a little discussion with anybody else who has any thoughts about HTML output of Isabelle theories.

Best wishes,
John