David,
On 4 Mar 2008, at 18:29, David Matthews wrote:
Rob Arthan wrote:
If you write your own read-eval-print loop using PolyML.compiler, you may want to treat exceptions raised during the eval stage specially. However you can't currently stop Poly/ML printing out the exception. It seems appropriate to me to use negative values of the error depth control to do this. I note that the error depth also influences syntax-checking and type-checking error messages, but I can't see why anyone would want to suppress those.
Rob, Would it make sense to use print_depth rather than error_depth here and leave error_depth for compiler error messages? Then setting print_depth to zero could have the effect of suppressing the printing of exceptions in the same way that it suppresses the printing of top-level declarations. So print_depth applies to printing run-time values and error_depth to compile-time.
No, that definitely wouldn't make sense for me. ProofPower wraps a pre- and post-processor around the ML read-eval-print loop, essentially to extend the lexis so that object language quotations become part of the language. Any ML value can be returned, so I need the compiler to pretty-print the value.
However, exceptions are different: I can print them myself and sometimes I just want to catch them and take special action. E.g., there is an exception to terminate my read-eval-print loop and return to the Poly/ML one - in that case it is slightly confusing to the user to see the exception message printed by the compiler.
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.
That would allow your own read-eval-print loop to do what it liked. Since the depth of any structure printed by General.exnMessage is affected by print_depth rather than error_depth if I made this change I would also use print_depth to suppress exception printing.
Regards,
Rob.