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

# HG changeset patch # User David Greenaway david.greena...@nicta.com.au # Date 1364864695 -39600 # Node ID 27bd348e777a3ffa4a4bf5bb18faa0a8428e468f # Parent d40aec502416a0eaa094e5aef1f317f7c4867852 Fix top-level printing of exception messages containing forced-line breaks. Both Isabelle and

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

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 //