Updated

2 files changed, 19 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 984f7ab4..a5bb26d5 100644
--- a/CHANGES
+++ b/CHANGES
@@ -15,6 +15,12 @@
 
 *** Improved behaviour of electric terminator
 
+*** Point never moves if proof-follow-mode is 'ignore.
+
+  Previously it was always moved when an error occurred.
+  It's nicer to do this manually if you like this mode,
+  using M-x proof-goto-end-of-locked.
+
 *** Efficiency improvement in parsing
  
   Also works around crash bug in xemacs-21.1.7/SuSE.
@@ -37,10 +43,16 @@
 
 ** Isabelle Changes
 
+*** More code from Isamode has been merged into Proof General
+
+ Particularly: the user now can choose a logic image from inside PG.
+
 *** Fix for stack overflow in regexp which occurred with large proof states
 
 ** Isar Changes
 
+*** Fix for stack overflow in regexp which occurred with large proof states
+
 ** HOL Changes
 
 *** Output decoration improvements.
diff --git a/todo b/todo
index 50f8b32f..ce7db622 100644
--- a/todo
+++ b/todo
@@ -29,6 +29,8 @@ X (Low)		e.g. probably not worth spending time on
 
 *** Outstanding bugs to investigate
 
+A find C-c C-l binding and remove it.  Overriden with goto-end-of-locked.
+
 C Undoing comments with FSF Emacs weirdness.
  Noticed with Emacs 20.6.1.  Seems to affect all provers.
  Workaround:  use C-c C-RET or C-c C-r instead.
@@ -44,6 +46,11 @@ C Problem with startup for Coq and HOL.  See BUGS.
 *** Scheduled improvements for 3.2
 
 **** A Doc new bits: font lock keywords, filename %e, %r.
+  Added proof-{script,shell,goals,resp}-font-lock-keywords.
+  Presently used only in proof-easy-config, will put into other
+  mechanism for 3.2
+
+**** A Doc new bits: Isabelle settings mechanism, win32 support
 
 **** A Add a new keymap(s) for proof assistants.
   Presently they naughtily bind C-c <letter> which are reserved for