Dear friends of Poly/ML, or Standard ML in general,
Isabelle2013-2 is now 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/
It is mainly an environment for interactive and automated theorem proving, but the integration of Isabelle/ML into the Prover IDE makes it suitable for general Standard ML development (potentially in teaching scenarios).
After downloading / unpacking / running the main application of Isabelle/jEdit, the Documentation panel on the right-hand side gives quick access to Examples, notably src/HOL/ex/ML.thy for some Isabelle/ML basics.
The manual on Isabelle/jEdit in the same panel provides further details on the IDE, which is based on the jEdit text editor.
Makarius
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-o...
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
-
makarius＠sketis.net