On Sat, 20 Jun 2009, David Matthews wrote:
The model we've traditionally used for ML, or at least Poly/ML, is that of a sequence of files compiled in a defined order with each file providing some context for its successors. The context generally includes declarations in the global name space but can include other context such as the current working directory. This makes it more difficult for the IDE to know exactly what context to use for a particular source file. The reason this is important is that we want to be able to compile a source file when the user edits it so that the IDE can provide information about internal types and that's only possible if all the top-level declarations that the file expects are available.
This traditional ML model of "incremental compilation", i.e. compilation that is intertwined with execution, is exactly what is required for applications like Isabelle. It is one of the reaons why we could never use separate compilation versions of ML like MLton or MLkit.
An "Isabelle project" (which is called "session" in our terminology) consists of a collection of theory files that may also "use" ML text, either as separate files or embedded into our source format. This works by our own runtime invocation of the Poly/ML compiler.
For our ongoing Isabelle IDE efforts, we essentially assume that ML compilation can be invoked frequently and works more or less in real time (Poly/ML compilation is quite fast, especially if compared to the time for checking specifications and proofs in Isabelle.)
Fundamentally, the issue is how far should the user be required to change existing source code and manner of working in order to be able to use the IDE. Must each file contain just one top-level declaration? Is a file allowed to call OS.FileSys.chDir to change the current directory? Can a file declare its own version of "use" by wrapping up PolyML.compiler and then compiling some files with it? This is less of an issue for new code but there's a lot of existing code around.
In Isabelle/ML we now more or less assume that there are no chdirs and no side effects on refs. We are lucky enough to can afford this in our specific framework, which provides its own ways to manage context data without side effects.
Makarius