[isabelle-dev] html output of theories

[Lawrence Paulson]

Looks nice. Just the indenting needs fixing.
Larry

On 12 Apr 2014, at 11:58, John Wickerson <johnwickerson at cantab.net> wrote:

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