From 74a96331fb30d7d0b89558ec15cba2e0a859db20 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Sun, 30 Jun 2002 22:49:30 +0000 Subject: Reorg. Mention fontification bug. --- BUGS | 138 ++++++++++++++++++++++++++++++++++++------------------------------- 1 file changed, 75 insertions(+), 63 deletions(-) (limited to 'BUGS') 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. -- cgit v1.2.3