From ec3eaa1329f4f7712f6ae93f51bcb4d3d2bc8b2a Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 13 Sep 2000 15:53:52 +0000
Subject: Updated

---
 CHANGES | 19 +++++++------------
 todo    | 10 ++++------
 2 files changed, 11 insertions(+), 18 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.
 
diff --git a/todo b/todo
index 39e9bb7e..367060ea 100644
--- a/todo
+++ b/todo
@@ -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.
 
-- 
cgit v1.2.3