aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2000-09-13 15:53:52 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2000-09-13 15:53:52 +0000
commitec3eaa1329f4f7712f6ae93f51bcb4d3d2bc8b2a (patch)
tree524e078ff4e7176a7a2bfa848a320c80abe2f50f /CHANGES
parentc1d1708127e306d1035259e7ad830148e84885a1 (diff)
Updated
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES19
1 files changed, 7 insertions, 12 deletions
diff --git a/CHANGES b/CHANGES
index 98563824..2e573501 100644
--- a/CHANGES
+++ b/CHANGES
@@ -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.