On Wed, 26 Mar 2008, David Matthews wrote:
I've experimented with adding equivalent functions to the present PolyML.print and PolyML.makestring (from which General.exnMessage is derived) but with the name space to be used as an additional argument. The most general form would be something like: PolyML.printPretty: { value: 'a, nameSpace: nameSpace, stream: string->unit, depth: int, lineLength: int } -> () PolyML.formatAsString: 'a * nameSpace -> string
Because the compiler treats them specially this restricts the way they can usefully be incorporated into other functions. For example it's not possible to define fun makestring a = PolyML.formatAsString(PolyML.globalNameSpace, a) because this would capture the type of "a" as 'a and so it would only ever print "?".
Apart from the print functions the only other case where the global environment is used is the "debug" function. This is set using setDebugShell.
Maybe the above PolyML.printPretty with explicit name space argument will help a little bit for the particular problem of printing exceptions. But I also realize now that general print/makestring functionality is not fully addressed by this extra argument: the name space is not the actual environment value, only the record of access functions to an implicitly mutable table. So we need to manage the latter using ``setmp'' tricks anyway.
So a global configuration of the default name space, like PolyML.setPrintEnv but also for PolyML.compiler, could do the job. This is then a bit like configuring the global signal handler for the runtime system.
Alternatively, it could also be passed in as a parameter to PolyML.compiler but that is adding yet more arguments. But since most of the arguments to PolyML.compiler have sensible defaults I'm wondering whether it would be better to change the type of PolyML.compiler to use something like the threadAttribute settings in Thread.Thread.fork. PolyML.compiler would have type: (unit->char option) * compilerArgument list -> unit -> unit so the only compulsory argument would be the input stream and the others could be given in the list or left to default.
This looks like a good idea independently of the above issues.
| FileName of string (* Default is empty string i.e. interactive *) | LineNumber of unit->int (* Default is no line numbering *)
How about just one argument to produce an error message, depending on the present line number, e.g. MakeError of int -> string -> string or PutError of int -> string -> unit. This would allow to wrap up the position information in a way that the user interface understands, cf. the uniform Position.str_of (with optional markup) that we are using in Isabelle. (That function would include the constant file name information by itself.)
Makarius