Roger,
I think the short answer is to use the ProofPower exception mechanisms
for readable exception messages.
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.
If you process the supporting SML at the end of this message, you will
see when the user-supplied writers are used by Poly/ML:
compileString "\"abc\";";
(* CPOutStream writer used for normal text output *)
compileString "PolyML.print \"abc\";";
(* CPPrintStream writer used for PolyML.print output *)
compileString "raise General.Fail \"abc\";";
(* Note that exception message does not go via
either CPOutStream or CPPrintStream writers *)
I think Rob may have more info on why Poly/ML is like this.
Phil
(* Supporting SML *)
local
val input = ref ""
val pos = ref 0
fun setInput s = (input := s; pos := 0)
fun readInput () =
SOME (String.sub (!input, !pos)) before pos := !pos + 1
handle
Subscript => NONE
open PolyML.Compiler
in
fun compileString s = (
setInput s;
PolyML.compiler
(readInput,
[CPOutStream (fn s => app print ["\nCPOutStream[", s, "]"]),
CPPrintStream (fn s => app print ["\nCPPrintStream[", s, "]"])])
()
)
end;
(* End of supporting SML *)
Roger Bishop Jones wrote:
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
Is there a way to get string valued exceptions to print
extended characters correctly?
Roger Jones
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
iEYEARECAAYFAk2op9wACgkQpS+qcQX1oA+2vQCdEqFqkt4z1U3ZVJsF5TLxUy9f
vMkAoJcf2wlbyiygoHi0FteGVWAaFYsP
=LuxB
-----END PGP SIGNATURE-----
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
