aboutsummaryrefslogtreecommitdiffhomepage
path: root/BUGS
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>1999-12-13 17:38:04 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>1999-12-13 17:38:04 +0000
commit1764b9fdda5d3e58adab3a52125f4556f546f1ac (patch)
treeebee8b02b41986a764ddc6395cf4dce12a577c41 /BUGS
parent0fcf38d3da5f8da4d0c69f6fde7b811edfebf56b (diff)
Added two new bugs.
Diffstat (limited to 'BUGS')
-rw-r--r--BUGS14
1 files changed, 14 insertions, 0 deletions
diff --git a/BUGS b/BUGS
index afb4152a..8585b9f6 100644
--- a/BUGS
+++ b/BUGS
@@ -11,6 +11,20 @@ See also: http://www.dcs.ed.ac.uk/home/proofgen/ProofGeneral/BUGS
Generic problems
================
+* If you have problems using Mule versions of FSF Emacs (beware
+setting standard-display-european): Pascal Brisset suggests adding
+this line to .emacs should help:
+
+ (setq process-coding-system-alist '(("" . no-conversion)))
+
+* If the proof assistant goes into a loop displaying lots of
+information, it may be difficult or impossible to interrupt it,
+because Emacs doesn't get a chance to process the C-c C-c keypress
+or "Stop" button push (or anything else). In this situation, you
+will need to send an interrupt to the Isabelle process from another
+shell. This problem can happen with looping rewrite rules in the
+Isabelle simplifier, when tracing rewriting.
+
* Highlighting script buffers in recent versions of FSF Emacs is a
mess. The underlying text property implementation has changed
and it seems difficult to get the desired behaviour of highlighting