Rob Arthan wrote:
On 16 Apr 2011, at 02:55, Phil Clayton wrote:
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?).

Good point - I forgot that the read/eval/print loop is catching all exceptions. It looks like exnMessage is just creating strings with PolyML.makestring which (I think) is using String.toString to print the body of strings (see basis/String.sml, lines 882-886.) I was going to suggest just installing a new printer for the type string that does not escape the ProofPower printable characters - I tried it and it works - but have been sidetracked looking into the writer side of things.

Phil




_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to