On Wed, 6 Jan 2016, David Matthews wrote:
Most of the documentation relates to the signatures of library functions. It would be really nice to be able to have the descriptions of the functions contained in comments in the library source itself and then have a program that would automatically turn the ML signature and the special comments into HTML. I think there are such things for other languages although I've never used them. Is there such a thing for ML? This would make it much easier to keep the source code and the documentation in sync.
Many people think that Isabelle is a theorem prover, but it is actually a document preparation system with formal checking of embedded languages. Isabelle/ML (or Standard ML) is part of that.
That is *not* for pretty printing of raw sources, but for writing regular documents that refer to things defined elsewhere. Output is mainly PDF-LaTeX -- HTML is lagging behind in recent years.
Here is an example:
http://isabelle.in.tum.de/repos/isabelle/raw-file/Isabelle2016-RC0/src/Doc/I... http://isabelle.in.tum.de/website-Isabelle2016-RC0/dist/Isabelle2016-RC0/doc...
There is also Markdown-like notation: see <^item>, <^enum>, <^descr> in the source, which is rendered with nice Unicode glyphs in the prover IDE. So a realistic view on the source above requires the full application, see http://isabelle.in.tum.de/website-Isabelle2016-RC0
For me, the benefit of the formal markup of the document outline and pseudo-markup for the text content is that it is managed by Isabelle and the IDE.
Makarius