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. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev