[isabelle-dev] html output of theories

[John Wickerson]

Thanks Larry. Sorry, but I don't see any difference in the indentation, at least not in safari or chrome. Can you point out a line that's wrong?

Sent from my iPhone

> On 12 Apr 2014, at 17:01, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> 
> 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
>