aboutsummaryrefslogtreecommitdiffhomepage
path: root/BUGS
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2004-04-17 12:04:03 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2004-04-17 12:04:03 +0000
commit18d5bdb4e852efe0338d793ba99a2b7ee34e08c7 (patch)
tree2d2a472e21ffa9caf43ebfe3f2d0f9bdb31ce4d0 /BUGS
parent90ea182ba3992b16101d62725449f36d66e62bbd (diff)
Note about font-lock problem in XE 21.4.x x<11
Diffstat (limited to 'BUGS')
-rw-r--r--BUGS47
1 files changed, 35 insertions, 12 deletions
diff --git a/BUGS b/BUGS
index 7c83c59e..a39f5a7b 100644
--- a/BUGS
+++ b/BUGS
@@ -80,24 +80,37 @@ to edit a file as it is being read by the proof assistant!
-* Problems with particular Emacs versions [mostly historical]
+* Problems with particular Emacs versions
-** X-Symbol on GNU Emacs
+** General note: PLEASE CHECK YOUR EMACS IS UP TO DATE
-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.
+Most of the issues below relate to old Emacs versions. Proof General
+is already chock-full of patches for Emacs bugs, it's time to start
+removing these kludges rather than adding more. Feel free to report a
+bug which may be Emacs-related: from now on I will add a note here
+rather than try to investigate older Emacsen and add more patches
+to the code.
+
+** XEmacs font-lock problem in earlier versions of XEmacs 21.4
+
+When reloading (with C-x C-f) an already loaded script file that has
+been changed on the file system you see the error:
+
+ (1) (warning/warning) Error caught in `font-lock-pre-idle-hook':
+ (wrong-type-argument markerp nil)
+
+As a result fontification, etc, fails. Workaround: use C-x C-v
+instead. This problem has gone away since 21.4.12 or so.
-** Emacs menus: options not updated dynamically, positions erratic, etc.
+
+** GNU Emacs menus: options not updated dynamically, positions erratic, etc.
Also, proof assistant specific menus only appear in scripting buffer.
-These are drawbacks with GNU Emacs menu support.
+These are drawbacks with GNU Emacs menu support on early versions. As
+of Emacs 21.3, these glitches have gone. (Although bugs have been
+known to return).
-** Emacs faces sometimes faulty, esp in console mode
+** GNU Emacs faces sometimes faulty, esp in console mode
Emacs support is let down in console mode, because faces are not
implemented there. (XEmacs can use colours and underline in console
@@ -117,6 +130,16 @@ 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.
+** X-Symbol on GNU Emacs
+
+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.
+
** As of GNU Emacs 20.3, multi-byte character codes are used.
This breaks some of the code in Proof General, which is turned off in