[isabelle-dev] NEWS: Isabelle support for Standard ML (fwd)

[Makarius]

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 
everything myself.


Automatic compilation management could also work, but the Isabelle IDE 
needs an excplit DAG (i.e. the "theory graph") before it starts doing 
anything.


 	Makarius

---------- 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.

Larry

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.