[isabelle-dev] html output of theories
makarius at sketis.net
Wed Apr 16 15:14:18 CEST 2014
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.
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.
More information about the isabelle-dev