Rob Arthan wrote:
Actually, I think the code in COMPILER_BODY that prints out the exception information was written before General.exnMessage existed. From what I can tell it should be possible to remove that code and instead print the exception information in the Poly/ML read-eval-print loop.
That would be a much better solution I think, since most users won't want to suppress exception messages altogether but may want to limit the amount of information in them. Your read-eval-print loop would also then provide a fully-featured prototype for anyone trying to write their own.
Rob, 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. The new version of PolyML.compiler has type: {getChar: unit -> char option, fileName: string, nameSpace: PolyML.NameSpace.nameSpace, putString: string -> unit, lineNumber: unit -> int} -> unit -> unit
getChar is used for the input stream. Unlike the old PolyML.compiler this returns a char option rather than a string. NONE is used to signal end-of-file. putString is, as before, the output stream. fileName is the name of the file used in error message. The empty string indicates an interactive stream. lineNumber is used indicate the source line in an error message. Returning zero suppresses this. 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. PolyML.make works by interposing between the compiler and the global space. When a structure, functor or signature name is looked up it checks whether the entity is up-to-date and may recursively invoke the compiler before eventually returning the recompiled entity. It might be possible to use this for some form of quotation or anti-quotation.
This is still experimental but I think it's going in the right direction. I've produced updated versions of the import files for x86-32 and x86-64. I still need to do that for the other architectures.
Regards, David.