[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 

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.


More information about the isabelle-dev mailing list