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
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to