Updated.

1 files changed, 8 insertions, 13 deletions

diff --git a/BUGS b/BUGS
index 3008e61a..6f25bc57 100644
--- a/BUGS
+++ b/BUGS
@@ -82,12 +82,15 @@ to edit a file as it is being read by the proof assistant!
 
 * Problems with particular Emacs versions [mostly historical]
 
-** Buggy output fontification with Emacs 21.2 / X-Symbol 4.X
+** X-Symbol on GNU Emacs
 
-Output colouration may spill into adjacent symbols when X-Symbol
-support is switched on.  X-Symbol 4.X isn't yet finished, and will
-only officially support Emacs from 21.4 onwards.  It may work with
-Isabelle for Emacs 21.X but please don't try it with other provers.
+X-Symbol 4.X isn't finished yet and will only supported GNU Emacs from
+GNU Emacs 21.4 onwards.  For the time being there are a few minor
+glitches (buffer gets modified during decoding,
+subscripts/superscripts don't work, output colouration may spill into
+adjacent symbols...), but on the whole it is quite usable (and
+rather faster than XEmacs).  For more information about X-Symbol,
+see http://x-symbol.sourceforge.net.
 
 ** Emacs menus: options not updated dynamically, positions erratic, etc.
 
@@ -100,14 +103,6 @@ Emacs support is let down in console mode, because faces are not
 implemented there.  (XEmacs can use colours and underline in console
 mode)
 
-** XEmacs 21.1.9 on Win32
-
-Some strange problems reading files with this version of Emacs. Gives
-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 GNU Emacs 
 
 Beware setting standard-display-european: Pascal Brisset suggests