diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-07-14 13:12:23 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-07-14 13:12:23 +0000 |
| commit | 8c67b17ae0d8eda7d2a779989ea820c1e8d1bafd (patch) | |
| tree | 3580b3dab386f47c2fbd43ec3bf9b859890c5c60 /BUGS | |
| parent | 553f56d5d0ddc88c219c0fb22cb0ace0e8177441 (diff) | |
Tracing bug
Diffstat (limited to 'BUGS')
| -rw-r--r-- | BUGS | 15 |
1 files changed, 0 insertions, 15 deletions
@@ -20,21 +20,6 @@ versions, and those which only apply to particular versions. If you have more than one theorem with the same name in a buffer, their proof visibilities are controlled together. -** Issues with tracing mode (Isabelle only) - -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. - ** If the proof assistant goes into a loop displaying lots of information It may be difficult or impossible to interrupt it, because Emacs |