On Fri, 12 Dec 2014, Lucas Dixon wrote:
If you really want plain SML'97, then your best approach might be to
cannibalize Isabelle, pull out it's build system, and hack it's IDE a
little, and build your own SML'97 IDE. But this is probably quite a big
task.
Lucas, we've had many private discussions about that in the past, so lets
continue that publicly now.
What I've done in Isabelle2014 is the following:
* The Isabelle/Pure/PIDE environment is able to include strict SML'97
modules with their own toplevel ML name space: command 'SML_file'.
* It is possible to move toplevel bindings back and forth between the
Isabelle/ML and SML environment: command 'SML_import' and
'SML_export'.
In $ISABELLE_HOME/src/Tools/SML/Examples.thy there are some tiny examples
to illustrate that, e.g. the Isabelle/ML function Output.writeln is
re-used for SML to make output actually visible in the IDE and not get
lost on bare stdout via TextIO.print etc.
Another example is to re-use the Isabelle/ML Par_List.map combinator for
SML: it provides already some realistic parallel programming facility at
very little cost for an existing program.
Many things can be imagined beyond this:
* Some way to single-out SML programs for standalone builds, without the
Isabelle or PIDE framework around it.
* Some way to allow multiple simultaneous arguments for SML_file: the
compiler could be instructed to find signature/structure/functor
definitions according to certain naming conventions of source files,
without requiring the usual sequential load order of the logical
framework.
* Emulation of the SML/NJ make system, to allow easy inclusion of other
SML projects.
As a start, I am considering to make a stand-alone Isabelle/SML/PIDE
distribution next time. I have already reduced the disk footprint
drastically, by using only JRE and not full JDK, and without the
Isabelle/HOL image it will come out rather small.
Makarius
----------------------------------------------------------------------------
http://stop-ttip.org 1,143,454 people so far
----------------------------------------------------------------------------
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
