-*- mode:outline -*-

* Isabelle/Isar Proof General Bugs

See also ../BUGS for generic bugs.

** Issues with tracing mode 

1. Large volumes of output can cause Emacs to hog CPU spending
all its time processing the output (esp with fontifying and X-symbol
decoding).   It becomes difficult to use normal editing commands,
even C-c C-c to interrupt the prover.  Workaround: hitting C-g,
the Emacs quit key, will interrupt the prover in this state.
See manual for further description of this.

2. Interrupt response may be lost in large volumes of output, when
using pty communication.  Symptom is interrupt on C-g, but PG thinks
the prover is still busy.  Workaround: hit return in the shell buffer,
or set proof-shell-process-connection-type to nil to use piped
communication.