On 16 Apr 2011, at 02:55, Phil Clayton wrote:
> I think the short answer is to use the ProofPower exception mechanisms for
> readable exception messages.
Yes! Does this give you any problems, Roger?
> I presume you want e.g.
> raise General.Fail "%forall%";
> to show the for all symbol rather than \181. Unfortunately it seems Poly/ML
> does not allow this. Whilst the Poly/ML compiler interface allows
> applications to specify their own writer functions for writing text output
> from the compiler, these user-supplied writers are bypassed for the exception
> text output. Therefore the ProofPower writer can't be used here and,
> unfortunately. Poly/ML thinks \181 is unprintable so escapes it.
That is not exactly what happens, but the effect is the same. The ProofPower
reader/writer is calling the compiler and handling any exceptions raised. If it
gets an exception defined by ProofPower, like BasicError.Fail - the one raised
by the function fail - then it can take special action. If it gets some other
exception, it calls General.exnMessage from the standard basis library to find
out what to print, and the Poly/ML implementation of General.exnMessage just
formats the exception as if it were about to print it in its read/eval/print
loop. ProofPower could treat General.Fail specially, but that probably isn't
what Roger wants (is it?).
Proofpower mailing list