diff options
| -rw-r--r-- | BUGS | 32 | ||||
| -rw-r--r-- | CHANGES | 24 | ||||
| -rw-r--r-- | todo | 23 |
3 files changed, 42 insertions, 37 deletions
@@ -37,15 +37,18 @@ the best of all possible worlds, switch to XEmacs. * 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. This could effect -forthcoming versions of XEmacs (but hasn't as far as XEmacs 21.1). -Workaround: use FSFmacs 20.2, or XEmacs 20.4/later. +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. * Using C-g can leave script management in a mess. The code needs to have some regions protected from Emacs interrupts. -Workaround: Don't type C-g while script management is processing. If -you do, use proof-restart-scripting. +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 due to read-only restrictions of the protected region. This is an inherent @@ -130,6 +133,9 @@ mechanism. * User defined tactics cannot be retracted. Workaround: you may need to retract to the beginning of the proof. +* Surely others that aren't mentioned here. Please report them +to proofgen@dcs.ed.ac.uk. + Isabelle Proof General Bugs =========================== @@ -144,15 +150,5 @@ interface unless you use your own "goal" or "qed" forms. * Blocking when processing multiple files, beginning from a .ML file. Proof General will block the Emacs process when it is waiting for a -theory file (and it's ancestors) to be read. To avoid this, assert -the theory file rather than the ML file, or use C-c C-s to start -scripting (which triggers reading the theory) before using one of -the assertion commands. - -* Cut-and-paste from Isabelle output (e.g. goals buffer) is -problematic. You will find that this inserts otherwise-invisible -special characters into the script buffer, which are used to do the -highlighting. If you really need to do cut-and-paste, customize the -variable proof-shell-leave-annotations-in-output to nil. -Unfortunately this will turn off variable colouring. - +theory file (and it's ancestors) to be read as scripting is turned +on. To avoid this, assert the theory file rather than the ML file. @@ -37,12 +37,15 @@ Generic Changes (it was too easy for the user to accidently type C-u C-c C-u !) * User options have been re-organized and renamed to be - more suggestive. "Active terminator minor mode" is now - called "electric terminator". Boolean options can be + more suggestive. Boolean options can be toggled from the menu and saved with "Save options" on the ordinary Emacs "Options" menu. (Others can be set via Customize). - + +* "Active terminator minor mode" is now called "electric + terminator". It has one setting for all buffers, and + you can customize it if you want it permanently on. + * Command C-c C-t (proof-try-command) removed in favour of C-c C-v (proof-execute-minibuffer-cmd), which now uses the filter proof-state-preserving-p to check that a command is safe. @@ -172,13 +175,16 @@ Internal changes for developers to note * proof-shell-leave-annotations-in-output variable has been added. This allows quick and dirty mark up of output from the proof assistant using special characters with codes above 128 and - font-lock. Such characters are hidden from display in the + font-lock. Such characters are removed from display in the output buffers. - However, it is NOT recommended to use this mechanism, because - it breaks the usability of cut and paste (which copies the - special characters). Furthermore the entire mechanism of - using special character codes is fragile and needs replacing - in future versions of Proof General! + However, it is NOT recommended to use this mechanism heavily, + because the entire mechanism of using 8 bit character codes as + "special" characters is fragile and needs replacing in future + versions of Proof General! + +* proof-font-lock-zap-commas has been added to control whether + or not the excrutiating font-lock hack to unhighlight commas + is enabled. * Many code cleanups and improvements. @@ -72,6 +72,11 @@ B BUGLETS: - If Proof General is loaded with M-x load-library, it gets set up for *no* proof assistant!! - Repetition of "load .emacs" on menu bar even when it's been loaded. + - Response buffer doesn't scroll to display o/p (it does for debug msgs, + oddly). This might have been a 1998 design decision. + Maybe it should be a user option? + + - XEmacs pg forces on font-lock! B SMALL DELTAS: - Consider setting proof-mode-for-script automatically? @@ -81,6 +86,11 @@ B SMALL DELTAS: (problem synchronizing) - Difference in menubar appearance depending on whether X-Symbol is loaded before Proof General or not. + - Improvements to script navigation commands. Would like some + uniformity with proof-find-next-terminator, and a better + implementation. Maybe we have four commands: find command start, + command end, and move to next command/previous command. + B Have seen "confused" bug: shows up when do lots of C-c C-n as process is starting up. @@ -100,11 +110,6 @@ B Making undoing better. D Why don't PG's minor modes appear on XEmacs minor mode menu? (C-right on status bar) -A Markus's bug reminder list: - - cut&paste from hilited Isabelle output includes invisible specials; - - c-c c-c does not work reliably; - - c-c c-a is broken; - A Bugs in x-symbol support: - visiting multiple files sometimes doesn't display them properly (setq x-symbol-8bits nil) needed? @@ -143,11 +148,9 @@ C C-x C-v does not seem to run kill buffer hooks properly: at (e.g.) a completely processed file doesn't get added to the included files list. Auto retraction appears to work. -B Nested error problem: conceptually, activate scripting should fail - if the hook function which causes loading of more files (for isabelle) - fails. Maybe fix by adding a new piece of state: - "proof-shell-error-flagged" and testing it before allowing - scripting to start. +B Now we have proof-shell-error-or-interrupt-seen flag, we maybe don't + need proof-shell-handle-error-hook: presently only use is in Plastic + to set a similar flag. B Add something to better document two-buffer versus three-buffer interaction modes, and the use of proof-window-dedicated to |