On Fri, 14 Mar 2008, David Matthews wrote:
I've spent a while this week reorganising the interface between the compiler and the read-eval-print loop. Up till now the read-eval-print loop has been compiled as part of the compiler. That has limited the extent to which it has been possible to replace the loop with your own version since many of the hooks weren't available. I've now changed it so that only a limited version of the loop is used when compiling the basis library and the final, fully featured, version is compiled in at the end. The new version is in basis/FinalPolyML.sml in the current CVS.
As part of this I've changed PolyML.compiler to include all the arguments it needs and removed PolyML.compilerEx. This is an incompatible change which will affect Isabelle.
We have now catched up with these changes. So far it works without any problems.
The new argument is nameSpace. In most cases this can just be set to PolyML.globalNameSpace which will look up values in the normal ML name space and enter them there, but it is possible to set up your own name space or interpose one between the compiler and the global space.
This sounds very interesting. It looks like it will finally enable proper management of ML bindings invoked within Isabelle, observing the hierarchical structure of theories, admitting proper undo/redo, and working smoothly with multithreading.
The only concern is the global PolyML.setPrintEnv for General.exnMessage and PolyML.print. Is there an easy way to get a purely functional interface for passing the name space? Otherwise we need to apply the usual tricks with our setmp and CRITICAL markup.
Makarius