Thanks for the update! I'm going to try and update TheoryMine to the latest Isabelle, that way I'll get to play with all that cool new work you've been doing :)
On 13 December 2014 at 02:15, Makarius <makar...@sketis.net> wrote: > 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
