# Re: [isabelle] Help file for commands such as "declare [[show_types]]" because jEdit lacks PG features

*To*: Makarius <makarius at sketis.net>
*Subject*: Re: [isabelle] Help file for commands such as "declare [[show_types]]" because jEdit lacks PG features
*From*: Johannes Hölzl <hoelzl at in.tum.de>
*Date*: Fri, 01 Jun 2012 12:04:30 +0200
*Cc*: cl-isabelle-users at lists.cam.ac.uk
*In-reply-to*: <alpine.LNX.2.00.1205302058520.20590@macbroy21.informatik.tu-muenchen.de>
*Organization*: Technische Universität München
*References*: <4FBD5EED.1060902@gmx.com> <alpine.LNX.2.00.1205240045560.25549@macbroy21.informatik.tu-muenchen.de> <4FBD83B6.9070000@gmx.com> <4FBDD626.6010301@in.tum.de> <4FC031AC.1090001@gmx.com> <5D4DE228-8338-400C-A359-91F7DE9062E7@nicta.com.au> <4FC038E3.8040804@gmx.com> <4FC47ACC.5070704@in.tum.de> <4FC64C54.3070507@gmx.com> <4FC65183.3030509@in.tum.de> <alpine.LNX.2.00.1205302058520.20590@macbroy21.informatik.tu-muenchen.de>

Am Mittwoch, den 30.05.2012, 21:19 +0200 schrieb Makarius:
[..]
> Over all these years there has been a tension of HTML vs. PDF. I
> originally preferred proof documents with proper typesetting and
> pagination, but this now gets in the way for fully formal online text.
>
> My hope is that someone who really understands HTML4/CSS2 or HTML5/CSS3
> could give some hints how to make high-quality rendering of formal
> documents like the Isabelle manuals, or any other Isabelle document
> from applications.
This reminds me on MathJAX which was posted a couple of month ago on
this mailing list:
http://www.mathjax.org/demos/tex-samples/
The TeX sample look quiet impressive, and it looks like even inline TeX
works. They also have a solution for copy & paste:
http://www.mathjax.org/demos/copy-and-paste/
However MathJAX only interprets the LaTeX math-mode, I have no idea how
much work it is to transform entire documents into HTML using Tex4HT,
latex2html, ... And I think Isabelle currently does not produce math
output for terms.
- Johannes

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*