[isabelle-dev] html output of theories

[John Wickerson]

Hm, it seems that different browsers interpret the CSS "white-space" property in different ways. (Who'd have thought?) It's better now, thanks for pointing it out.

John

On 12 Apr 2014, at 17:55, Lawrence Paulson <lp15 at cam.ac.uk> wrote:

> I see no indentation at all, e.g.
> 
> 
> enriched_type map: Option.map proof -
> fix f g
> show Option.map f o Option.map g = Option.map (f o g)
> proof
> fix x
> show (Option.map f o Option.map g) x= Option.map (f o g) x
> by (cases x) simp_all
> qed
> next
> show Option.map id = id
> proof
> fix x
> show Option.map id x = id x
> by (cases x) simp_all
> qed
> qed
> 
> (in Safari)
> 
> Larry
> 
> On 12 Apr 2014, at 17:18, John Wickerson <johnwickerson at cantab.net> wrote:
> 
>> 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
>>> 
>