Custom Query (361 matches)
Results (43 - 45 of 361)
| Ticket | Resolution | Summary | Owner | Reporter |
|---|---|---|---|---|
| #315 | needmoreinfo | failure to show ML errors | ||
| Description |
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 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 |
|||
| #396 | fixed | error in proof-shell-insert-hook docstring | ||
| Description |
Hi, this docstring mentions the callbacks init-cmd and interactive-input. These seem not to exist any more. It does not mention proof-shell-set-silent and proof-shell-clear-silent. Bye, Hendrik Tews |
|||
| #371 | fixed | electric terminator mode broken | ||
| Description |
Electric terminator mode isn't working anymore with PG 4.0. When I type a period nothing happens. |
|||
