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/Implementation/ML.thy
http://isabelle.in.tum.de/website-Isabelle2016-RC0/dist/Isabelle2016-RC0/doc/implementation.pdf
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
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
