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

Reply via email to