[isabelle-dev] html output of theories

[Makarius]

On Tue, 15 Apr 2014, Christian Sternagel wrote:

> (3) This is what we all use every day, right? So this should be most 
> sophisticated (and already is, I think). Presentation wise the only 
> negative point I can think of, is that ugly LaTeX code is mostly 
> unreadable in the theory-file, while I need it sometimes for (1). In 
> that respect it would be wonderful if either Isabelle/jEdit would 
> magically present the result of TeXing or support nicely rendered syntax 
> for formatting

Proper integration of the latex document preparation process into the 
Prover IDE has indeed a high priority in the pipeline.  I have started to 
revisit it mentally shortly after the release in December 2013.  It 
remains to be seen if I manage to do something in the coming weeks.  (In 
June I will be mostly on vacation, and afterwards we have to converge 
towards the Isabelle2014 release.)

The spell-checker is already part of the document preparation improvement 
effort.


> I think there is no way around LaTeX when it comes to rendering 
> formulas. Maybe there is. Do you know MathML?

MathML is one of these "future technologies" that retain that status for 
decades, without ever getting there.  I remember that it was advertized as 
the next big thing for Math on the Web shortly after HTML and Mosaic / 
Netscape 1.x became popular in 1991 or 1992.

I am occasionally involved in the CICM/MKM conference, where MathML is one 
traditional topic.  Just 1-2 years ago someone of the insiders pointed out 
that the half-baked support for MathML in major browser engines (Mozilla 
or Webkit) was about to be *diminished* or *removed* because nobody is 
there to pursue this seriously.


 	Makarius