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
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
