Reorg. Mention fontification bug.

1 files changed, 75 insertions, 63 deletions

diff --git a/BUGS b/BUGS
index 17268bb3..eb39f2e4 100644
--- a/BUGS
+++ b/BUGS
@@ -15,13 +15,6 @@ versions, and those which only apply to particular versions.
 
 * Generic problems, for all Emacs versions
 
-** Looping in Emacs 21.2
-
-Several (odd) circumstances cause this version of Emacs to loop.
-For example, (setq-default column-number-mode t) before starting
-Emacs, or moving the cursor around in the *coq* buffer.
-It seems likely that these are Emacs bugs, workaround unknown.
-
 ** Visibility control doesn't distinguish theorems with same name.
 
 If you have more than one theorem with the same name in a buffer,
@@ -38,52 +31,67 @@ This problem can happen with looping rewrite rules in the Isabelle
 simplifier, when tracing rewriting.  It seems to be worse on 
 certain architectures, and slower machines.
 
-** Toolbar enablers for XEmacs 21, some artefacts.
+** Toolbar enablers unreliable on some platforms.
 
- There is a timing issue, so that occasionally the buttons are
- disabled/enabled when they shouldn't be.  An extra click on the
- toolbar solves this.
+Occasionally the buttons are disabled/enabled when they shouldn't be.
+An extra click on the toolbar may solve this.  If you have problems,
+please customize `proof-toolbar-use-button-enablers' to nil to
+disable the enablers. 
 
 ** Using C-g can leave script management in a mess.  
 
-  The code is not fully protected from Emacs interrupts.
-  Workaround: Don't type C-g while script management is processing.  
-  If you do, use proof-restart-scripting.
+The code is not fully protected from Emacs interrupts.
+Workaround: Don't type C-g while script management is processing.  
+If you do, use proof-restart-scripting.
 
 ** Outline-mode does not work in processed proof script files 
 
- Because of read-only restrictions of the protected region.  
- This is an inherent problem with outline because it works by 
- modifying the buffer.
- Workaround: none, nevermind.  (If it's hugely needed we could support
- modified outline commands).
-
-** Multiple file scripting is slightly vulnerable.
-
- Files are not locked when they are being read by the prover, so a long
- file could be edited and saved as the prover is processing it,
- resulting in a loss of synchronization between Emacs and the proof
- assistant.  Files ought to be coloured red while they are being
- processed, just as single lines are.   Workaround: be careful not
- to edit a file as it is being read by the proof assistant!
- (Only applies to Lego and Isabelle)
+Because of read-only restrictions of the protected region.  
+This is an inherent problem with outline because it works by 
+modifying the buffer.
+Workaround: none, nevermind.  (If it's hugely needed we could support
+modified outline commands).
 
 ** When proof-rsh-command is set to "ssh host", C-c C-c broken
 
- The whole process may be killed instead of interrupted.  This isn't a
- bug in Proof General, but the behaviour of ssh.  Try using rsh
- instead, it is said to forward signals to the remote command.
+The whole process may be killed instead of interrupted.  This isn't a
+bug in Proof General, but the behaviour of ssh.  Try using rsh
+instead, it is said to forward signals to the remote command.
 
 ** In tty mode, the binding C-c C-RET has no effect.  
 
- Workaround: manually bind C-c RET to 'proof-goto-point instead.
+Workaround: manually bind C-c RET to 'proof-goto-point instead.
+
+** Multiple file scripting is slightly vulnerable.
+
+Files are not locked when they are being read by the prover, so a long
+file could be edited and saved as the prover is processing it,
+resulting in a loss of synchronization between Emacs and the proof
+assistant.  Files ought to be coloured red while they are being
+processed, just as single lines are.   Workaround: be careful not
+to edit a file as it is being read by the proof assistant!
+
+
 
 * Problems with particular Emacs versions
 
+** Looping in Emacs 21.2
+
+Several (odd) circumstances cause this version of Emacs to loop.
+For example, (setq-default column-number-mode t) before starting
+Emacs, or moving the cursor around in the *coq* buffer.
+It seems likely that these are Emacs bugs, workaround unknown.
+Please contact us if you can help.
+
+** Buggy output fontification with Emacs 21.2 / X-Symbol
+
+Output colouration may spill into adjacent symbols when
+X-Symbol support is switched on.
+
 ** Emacs menus: options not updated dynamically, positions erratic, etc.
 
 Also, proof assistant specific menus only appear in scripting buffer.
-These are drawbacks with FSF Emacs menu support.
+These are drawbacks with GNU Emacs menu support.
 
 ** Emacs faces sometimes faulty, esp in console mode
 
@@ -98,53 +106,57 @@ spurious "end of internal input stream", or silently ignores parts of
 files.  Example is coq/coq.el which reads in fine on Linux.
 Solution: use a more recent version of XEmacs.  
 
-** If you have problems using Mule versions of FSF Emacs 
+
+** If you have problems using Mule versions of GNU Emacs 
 
 Beware setting standard-display-european: Pascal Brisset suggests
 adding this line to .emacs should help:
 
    (setq process-coding-system-alist '(("" . no-conversion))) 
 
-** Strict read only disabled by default in FSF Emacs.
 
-  Unfortunately strict read only is incompatible with font lock in
-  FSF Emacs, so it is disabled by default.  Instead, you get a warning message
-  if the locked region is edited.
+** Strict read only disabled by default in GNU Emacs.
 
-** In FSFmacs, spurious "Region read only" errors
+Unfortunately strict read only is incompatible with font lock in
+GNU Emacs, so it is disabled by default.  Instead, you get a warning message
+if the locked region is edited.
 
- Same problem as above, different symptom.
- When proof-strict-read-only is set and font lock is on, these
- errors are given which break font lock.   
- Workaround: turn off proof-strict-read-only, font-lock, or for
- the best of all possible worlds, switch to XEmacs.
+
+** In GNU Emacs, spurious "Region read only" errors
+
+Same problem as above, different symptom.
+When proof-strict-read-only is set and font lock is on, these
+errors are given which break font lock.   
+Workaround: turn off proof-strict-read-only, font-lock, or for
+the best of all possible worlds, switch to XEmacs.
 
 
 ** XEmacs undo in the script buffer can edit the "uneditable region"
 
-  Test case: Insert some nonsense text after the locked region.
-  Kill the line. Process to the next command.
-  Press C-x u, nonsense text appears in locked region.
-  Workaround: take care with undo in XEmacs.
+Test case: Insert some nonsense text after the locked region.
+Kill the line. Process to the next command.
+Press C-x u, nonsense text appears in locked region.
+Workaround: take care with undo in XEmacs.
+
+** As of GNU Emacs 20.3, multi-byte character codes are used.  
 
-** As of FSFmacs 20.3, multi-byte character codes are used.  
+This breaks some of the code in Proof General, which is turned off in
+case the suspicious looking function
+toggle-enable-multibyte-characters is present.  The code that is
+turned off deals with term markup for proof by pointing, which only
+affects LEGO at the moment.  This problem could affect forthcoming
+versions of XEmacs (but hasn't as far as XEmacs 21.4).  [Can anybody
+tell us if it affects Mule versions of Emacs?]  
 
-  This breaks some of the code in Proof General, which is turned off in
-  case the suspicious looking function
-  toggle-enable-multibyte-characters is present.  The code that is
-  turned off deals with term markup for proof by pointing, which only
-  affects LEGO at the moment.  This problem could affect forthcoming
-  versions of XEmacs (but hasn't as far as XEmacs 21.1).  Can anybody
-  tell me if it affects Mule versions of Emacs?  Workaround: for LEGO
-  pbp, use FSFmacs 20.2, or XEmacs 20.4/later.
+Workaround: for LEGO pbp, use GNU Emacs 20.2, or XEmacs 20.4/later.
 
 ** XEmacs sometimes has strange start-up delays of several seconds.
 
- Possibly due to face allocation, when running remotely and
- displaying on an 8-bit display.  One workaround (and in fact the
- recommended way of working) is to run XEmacs locally and only
- the proof assistant on your fast compute server, by setting 
- proof-rsh-command.
+Possibly due to face allocation, when running remotely and
+displaying on an 8-bit display.  One workaround (and in fact the
+recommended way of working) is to run XEmacs locally and only
+the proof assistant on your fast compute server, by setting 
+proof-rsh-command.