[isabelle-dev] html output of theories

Lawrence Paulson lp15 at cam.ac.uk
Sat Apr 12 18:55:14 CEST 2014


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




More information about the isabelle-dev mailing list