[isabelle-dev] NEWS: Isabelle support for Standard ML (fwd)
makarius at sketis.net
Mon Mar 31 18:24:55 CEST 2014
Larry, lets continue this in public, because it is of general interest.
At the moment the outermost wrapper for "SML projects" within
Isabelle/jEdit is some theory file with 'SML_file' commands.
It should be an easy programming exercise for anyone who wants to learn
how to make a small jEdit plugin, to turn that into some kind of "project
manager". The jEdit plugin repository has already a few such plugins, so
it could be taken as starting point.
I left this open for now, since it is somehow trivial, and I can't do
Automatic compilation management could also work, but the Isabelle IDE
needs an excplit DAG (i.e. the "theory graph") before it starts doing
---------- Forwarded message ----------
Date: Mon, 31 Mar 2014 17:17:07 +0100
From: Lawrence Paulson <lp15 at cam.ac.uk>
To: Markus Wenzel <makarius at sketis.net>
Subject: Re: [isabelle-dev] NEWS: Isabelle support for Standard ML
If you wanted to advertise it on functional programming mailing lists, I
think it would be helpful to eliminate the need for a theory file. I’m not
sure what alternative could be used; I never understood the SML/NJ
Compilation Manager, nor the Poly/ML equivalent.
On 31 Mar 2014, at 17:11, Makarius <makarius at sketis.net> wrote:
> The download is actually not so big, and without Isabelle/HOL as default
> image the self-build would last only a few seconds.
More information about the isabelle-dev