failure to show ML errors

[Lucas Dixon]

When compiling a fairly large amount of code loaded implicitly by a theory header, the processed text in the buffer goes red but PG fails to show error messages. Also, I often see:

Lisp nesting exceeds `max-lisp-eval-depth'

Which I guess might be related to it. If I change to the *isabelle* buffer, I can see the error and when/if I hit return, then the errors are shown as usual in the buffer.

This is tested with CVS version of PG and Isabelle 2009-1 pre-release: ​http://www4.in.tum.de/~wenzelm/test/isa2009-1-test/. For an example see:

svn co https://isaplanner.svn.sourceforge.net/svnroot/isaplanner/trunk IsaP-trunk

isabelle emacs IsaP-trunk/IsaPlanner/IsaP.thy

Then break one of the later ML files e.g. in IsaCosy.

[David Aspinall]

Sounds a bit like #274 but presumably something different. Could you paste/attach/email some of the output from the *isabelle* buffer?