diff options
| -rw-r--r-- | CHANGES | 19 | ||||
| -rw-r--r-- | todo | 10 |
2 files changed, 11 insertions, 18 deletions
@@ -4,7 +4,7 @@ ----- NB: this is a pre-release of PG 3.2. Bugs likely, please report ------ ------ PG 3.2 is scheduled for release in Autumn 2000. ----- +----- PG 3.2 is scheduled for release at the end of September 2000. ----- ** Generic Changes @@ -149,24 +149,19 @@ *** Removed proof-terminal-string to simplify command setting - [ONGOING] As a simplification of the code, and to allow possibility of PAs without a terminal string, more smoothly. It is now the responsibility of each proof assistant's customization to add proof-terminal-string to commands where necessary. -*** New parsing mechanism in testing +*** New parsing mechanism - To allow more flexible proof script syntax for new provers. - Also efficiency improvements. - This change results in a few known oddities at the moment, e.g. - process whole buffer leaves off last line. - Also broken with FSF Emacs. - To test it, do - (defalias 'proof-segment-up-to 'proof-segment-up-to-new) + See the PG Adapting manual for information about the new variations + possible for `proof-segment-up-to'. These are supported for XEmacs only, + since FSF Emacs lacks the useful fast primitives we use. *** Other minor things (interest only to independent developers of PG modes): - No need for match string 1 in proof-shell-proof-completed - Added proof-shell-pre-sync-init-cmd, see doc. + No need for match string 1 in proof-shell-proof-completed + Added proof-shell-pre-sync-init-cmd, see doc. @@ -292,7 +292,10 @@ X Solaris bugs: font locking and button enabling. place to do this that in the proof-shell-insert-hook (should be triggered by resize events). -*** B Implement proof-generic-find-and-forget +*** D Implement proof-generic-find-and-forget + <...>-count-undos, to simplify prover-specific code. + Complete reengineering of *-count-undos and + *-find-and-forget at generic level *** C X-Symbol: is there a function to input in the minibuffer using a token language? @@ -393,11 +396,6 @@ C New modules: - Fix proof-script-command-separator and proof-one-command-per-line flag, document them. -*** C Make and test generic versions of <..>-goal-command-p, - <...>-count-undos, to simplify prover-specific code. - Reengineer *-count-undos and *-find-and-forget at generic level - [5h] - *** D Fix INFO-DIR-ENTRY in doc/ProofGeneral.texi to put Proof General info file into a good place. |