[isabelle-dev] [PATCH 0 of 1] Fix top-level printing of exception messages containing forced-line breaks

[David Greenaway]

Hi all,

I have noticed that in c ertain circumstances both Isabelle/jEdit and
Isabelle/ProofGeneral will render certain constructs with a large number
of spaces in them.

The problem can be seen with the following testcase:

    definition "test a b ≡ undefined"
    notation (output) test ("test // (_) // (_)")
    ML {* raise (CTERM ("test", [@{cterm "test x y" }])) *}

The root cause is related to the interaction between Isabelle and
PolyML's pretty-printers. A problem arises when converting from
Isabelle's format to PolyML's format, in that the former supports
"forced line breaks" while the latter does not. The current solution is
to expand such line-breaks into a directive to print a large number of
spaces (99999, to be precise), preventing PolyML from fitting the spaces
on a line, and hence forcing it to produce a line-break.

This approach, unfortunately, falls down in two areas:
"PolyML.makestring" renders the large amount of spaces, producing
undesirable results. Similarly, "General.exnMessage" in PolyML simply
calls "PolyML.makestring", and hence has the same problem.

This attached patch fixes one instance of this problem by using an
alternative mechanism to pretty-print unhanded exceptions which prevents
the large number of spaces being rendered, fixing the problem above.

I would appreciate it if an Isabelle expert could review that patch and,
if acceptable, apply it to mainline. (This can be easily done with "hg
import <patch-file>").

The patch is based off the current Isabelle tip, which is d40aec502416
at time of writing.

Thanks so much,
David


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.