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 /isar | |
parent | 553f56d5d0ddc88c219c0fb22cb0ace0e8177441 (diff) |
Tracing bug
Diffstat (limited to 'isar')
-rw-r--r-- | isar/BUGS | 16 |
1 files changed, 15 insertions, 1 deletions
@@ -4,4 +4,18 @@ See also ../BUGS for generic bugs. -Nothing specific here. +** 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. + |