Phil/Roger, On 16 Apr 2011, at 02:55, Phil Clayton wrote:
> Roger, > > 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?). Regards, Rob.
_______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
