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