[isabelle-dev] html output of theories

[Makarius]

On Tue, 15 Apr 2014, Lawrence Paulson wrote:

> PIDE does an awful lot already, and I’d worry about burdening it with 
> yet more functions.

I know what you mean.  When David Aspinall started some PGEclipse 
experiments 10 years ago I made jokes about it, like Eclipse being not the 
darkening of the sun (or Sun as a company), but a black whole that sucks 
up ever more resources.  Today, a basic Eclipse application can be 
actually quite small compared to Isabelle/PIDE in its full glory.  E.g. 
see http://research.microsoft.com/en-us/um/people/lamport/tla/toolbox.html

Any of this JVM technology is so heavy and difficult to master that when a 
projects manages to reach the critical mass to work out in practice, it 
has to become a black whole.


> It’s easy to get PDF from HTML, provided the quality is high enough.

Producing high quality HTML is the problem here.  In the private prelude 
to this mail thread, I pointed out to John that an expert for HTML/CSS 
rendering is needed here. If some expert shows up, or someone wants to 
make himself an expert, that is fine.

Until that happens, we need to continue making the best out of the 
existing Isabelle/jEdit rendering engine, which is already ahead of early 
versions of Netscape from the late 1990-ies.  It also avoids the "static 
HTML" problem, because the rich information produced by the prover is 
easily accessible from Isabelle/Scala, and its rendering may depend on 
user interactions and GUI status.


 	Makarius