[ProofPower] Exceptions not translated for output - raw_diag_string in imp110?

[Phil Clayton]

Whilst looking at imp110, I see that the caught exception messages are printed using raw_diag_string. As these are not printed from within compile[12], their output does not go via writer, consequently text is not translated for output, e.g.

   plus_conv %SZT%Q%>%;



A more interesting example is

   use_string "plus_conv %SZT%Q%>%;";



Phil

I tried changing a few occurrences to use diag_string instead (see patch) and this seemed to solve the issue this those cases. The patch reduces the number of Qs in the exception message from 16 to 4 but would we expect the 4 Qs to reduce to 1? As ordinary users _must_ be aware that Q in a string is escaped as QQQQ, perhaps not?

patch-imp110.txt.gz
Description: GNU Zip compressed data

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