From 8c67b17ae0d8eda7d2a779989ea820c1e8d1bafd Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Sun, 14 Jul 2002 13:12:23 +0000
Subject: Tracing bug

---
 BUGS      | 15 ---------------
 isa/BUGS  | 15 +++++++++++++++
 isar/BUGS | 16 +++++++++++++++-
 3 files changed, 30 insertions(+), 16 deletions(-)

diff --git a/BUGS b/BUGS
index 80146e4b..eb39f2e4 100644
--- a/BUGS
+++ b/BUGS
@@ -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
diff --git a/isa/BUGS b/isa/BUGS
index 068e7fa9..b874a599 100644
--- a/isa/BUGS
+++ b/isa/BUGS
@@ -5,6 +5,21 @@
 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.
+
 ** set proof_timing is problematic
 
 It will make the goals display disappear during proof.  This is
diff --git a/isar/BUGS b/isar/BUGS
index 88d9b757..11564906 100644
--- a/isar/BUGS
+++ b/isar/BUGS
@@ -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.
+
-- 
cgit v1.2.3