Updated

2 files changed, 15 insertions, 5 deletions

diff --git a/CHANGES b/CHANGES
index 78ed39f7..77a1c310 100644
--- a/CHANGES
+++ b/CHANGES
@@ -29,13 +29,20 @@ Generic Changes
   otherwise be disabled.
 
 * Menus and keybindings have been reorganized.  
-  Now keybindings invoke the same functions as the toolbar.
-  In particular, C-c C-n and C-c C-u are simplified so that
+  Bindings C-c <letter> are being phased out; they are supposed
+  to be reserved for the user according to Emacs convention.
+
+* Keybindings for assert/retract now invoke the same functions as the
+  toolbar. In particular, C-c C-n and C-c C-u are simplified so that
   they always process or retract exactly one command, rather
   than one command beyond point.  Moreover, C-c C-u does not 
   take an optional argument to delete the retracted text
   (it was too easy for the user to accidently type C-u C-c C-u !)
 
+* New command C-c C-RET proof-goto-point which generalises
+  previous proof-assert-until-point to also do retracting if
+  point is in the locked region. 
+
 * User options have been re-organized and renamed to be
   more suggestive.  Boolean options can be
   toggled from the menu and saved with "Save options"
@@ -46,8 +53,8 @@ Generic Changes
   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
+* 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.
 
 * Terminal string now automatically added to command for C-c C-v 
diff --git a/todo b/todo
index 9ec16902..0162bf9c 100644
--- a/todo
+++ b/todo
@@ -75,7 +75,7 @@ B BUGLETS:
   - 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?
-
+  - are face defconsts still needed now we use defface?
   - XEmacs pg forces on font-lock!
 
 B SMALL DELTAS:
@@ -91,6 +91,9 @@ B SMALL DELTAS:
   implementation.  Maybe we have four commands: find command start,
   command end, and move to next command/previous command.
 
+C Make code robust against accidental deletion of response/goals
+  buffer.  Add functions proof-get-or-create-{response,goals}-buffer.
+  [30 mins]
 
 B Have seen "confused" bug: shows up when do lots of C-c C-n as
   process is starting up.