On Fri, 19 Jun 2009, David Matthews wrote:
We're not yet at the point of releasing this although much of the code
is in SVN so it is possible to try it out. A major issue we're
struggling with is exactly what constitutes a "project". For other
languages and IDEs there's a clear distinction between compilation and
run-time. With ML, though, compilation involves execution. Typically,
a project will involve calling "use" on various files but "use" is
actually being executed. Creating an ML structure also involves
execution.
Even in more mainstream IDEs, the "project management" often does not work
as smoothly as it should. For example, I often find myself "rebooting"
Netbeans/Scala just to get in sync with external changes to sources or
jars. Whatever we will do for Isabelle (which integrates theory sources
with ML programs), we intend to do better :-)
Anyway, concerning the most basic "use" functionality in Poly/ML, for us
the main question is about global effects. Since Poly/ML already allows
the client (Isabelle) to provide an implementation of the ML environment
(for toplevel types, vals, structures etc.), the remaining question is how
to handle updates on references.
In your own IDE implementations I have seen the use of saved heap images
to achieve undoable global state. I wonder if this could be somehow
internalized, e.g. heap snapshots as plain ML values?
Anyway, even then I am unsure of what exactly will be required for the
Isabelle/ML IDE. Right now, we say that "regular" ML text has to evaluate
in a pure manner, without any side effects (toplevel bindings are handled
as pure context update). In practice, ref updates are often used for
runtime configuration (setting global flags), and that is intentionally
not undoable.
Frequently ".ML" in upper case is used for ML source although case isn't
significant on Windows. ".sml" is also widely used.
Isabelle/ML always uses .ML; some years ago many people started to use
.sml and .sig (e.g. in SML/NJ and Moscow ML).
Makarius
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
