[isabelle-dev] html output of theories
Makarius
makarius at sketis.net
Mon Apr 14 13:37:21 CEST 2014
On Mon, 14 Apr 2014, John Wickerson wrote:
> After typing out lots of antiquotations and so on inside my
> "text{*...*}" and "header{*...*}" blocks, I would like to see what these
> will look like in the finished product. I don't want to print it out, so
> I have no interest in a boring monochrome paginated PDF -- I just want
> my theory to look like it does in Isabelle/jEdit, but with the
> antiquotations properly rendered.
That alone is just an omission of current Isabelle/jEdit. I've come
across this a few times recently, so expanded antiquotations are likely to
become part of the PIDE document model eventually. (A technical snag is
that the current programming interface for document antiquotations is for
generating raw Latex source.)
> And I think HTML is probably the right tool for that.
I have personally nothing against HTML, I am just ignorant of how it
really works.
A slightly different approach is to provide a Web view on PIDE, as seen in
http://clide.informatik.uni-bremen.de
The guys at Bremen also have some ambition for high-quality rendering,
althouth it requires many rounds of refinement and sophistication to
approximate the quality of the static PDF output.
Makarius
More information about the isabelle-dev
mailing list