The following might be interesting to people working with Standard ML on the Poly/ML platform.
The Isabelle2011 release includes an experimental Prover IDE based on Scala and jEdit that can be also used as one for Standard ML, thanks to the tight integration of Poly/ML into the prover environment. Thus semantic annotations produced by the Poly/ML compiler are presented as tool tips and hyperlinks in the source. This is a simple corollary of much more involved prover infrastructure, and David Matthews has provided some functionality to connect to that quite some time ago.
See http://isabelle.in.tum.de/download.html for the regular Isabelle download and installation instructions. An editor session can be started like this (from the shell):
Isabelle2011/bin/isabelle jedit -l Pure Test.thy
Then Test.thy file can be populated like this:
theory Test imports Pure begin
ML {* fun fact 0 = 1 | fact n = n * fact (n - 1); *}
ML {* fact 42 *}
end
Now it is possible to hover over the ML text while holding CONTROL (or COMMAND on Mac OS X) to see some of the content produced by the Poly/ML IDE support, rendered as tooltips and hyperlinks.
Here is another example:
ML {* length *}
Hovering with CONTROL/COMMAND will expose a hyperlink pointing to the Poly/ML library sources.
For non-prover people it might look a bit odd to embed ML text like that into a formal theory file. At a later stage there will be also management for individual ML files.
The document model is stateless as far as ML bindings are concerned. Global side-effects via reference variables are an exception to that. (In the Isabelle context mutable state is never used in application code.)
Anybody interested in the augmented Isabelle/ML itself should take a look at chapter 0 of http://isabelle.in.tum.de/dist/Isabelle2011/doc/implementation.pdf
There is also some support for parallel functional programming using futures, which did not make it into the manual yet. See http://www4.in.tum.de/~wenzelm/papers/parallel-ml.pdf for some overview.
Makarius