Custom Query (361 matches)

When processing larger portions (thousands of lines) of a Isabelle theory file (e.g. with goto point), the cpu is almost completely consumed by emacs (over 90%) and poly only has a few %. This makes interactive work quite annoying.

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.

with Isabelle2009-1 retract buffer does not work anymore:

* Outer syntax error: name declaration expected, * but command theory was found