Dear friends of Standard ML.
This is an update on the Standard ML facilities of the recent release of
Isabelle2014 (August 2014). Compared to Isabelle2013-2 (December 2013),
the Prover IDE based on Isabelle/jEdit has been greatly improved.
IDE support for both Isabelle/ML and official Standard ML (SML'97) allows
direct editing of programs that are assembled from separate ML files.
The enclosing theory merely serves as some kind of "project file". See
the Documentation/Examples panel in Isabelle/jEdit (bottom of the list).
Isabelle2014 is available from the usual mirror sites:
Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/
Munich (Germany) http://isabelle.in.tum.de/
Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle/
If we've had such IDE support on all major platforms 10 or 20 years ago,
SML might be a bit more popular today. For example, a web search of "SML
IDE" yields the following slightly odd page:
http://stackoverflow.com/questions/2036744/ml-ide-and-compiler-for-windows-or-linux
It mostly refers to some editors with plain and basic syntax highlighting,
not really IDEs. Maybe some enthusiasts of Poly/ML and Isabelle/PIDE can
help to vote up my (updated) answer on the SML IDE in Isabelle2014.
Makarius
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
