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
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
