Updated

2 files changed, 33 insertions, 17 deletions

diff --git a/CHANGES b/CHANGES
index 9f4307ab..3925765a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -12,10 +12,31 @@
      Two menu items "Show proofs" and "Hide proofs" apply to
      all the completed proofs in the buffer.
 
-     Notes: 
-      1. Proofs of theorems with the same name are not 
-         distinguished, visibility controlled together.
-      2. FSF Emacs implementation is flaky
+     NB: proofs of theorems with the same name are not 
+     distinguished, their visibility is controlled together.
+
+*** Command to insert last output as comment in proof script.
+
+     Sometimes it is useful to paste some of the output from
+     goals or response buffer into the proof script.  A new
+     function `pg-insert-last-output-as-comment' (C-c C-;)
+     inserts the last output and converts it into a comment
+     using `comment-region'.
+
+*** Changes to colours, mouse highlighting, echo help messages
+
+     Now `proof-locked-face' becomes a lighter cyan. This is
+     less obtrusive when editing proofs, but is not so visible
+     for demonstrating PG: if you prefer the old stronger colour, 
+     customize the face to "lightsteelblue2" using
+     M-x customize-face RET proof-locked-face.  
+
+     New face `proof-mouse-highlight-face' (default: darker blue
+     than locked region) is now used for mouse highlighting regions of
+     script. Less ugly than the previous default (green) highlight face.
+
+     Also, for XEmacs, there are now (trivial) help messages in echo
+     area describing the highlighted region under the mouse.
 
 *** Proof General startup script welcomes user
  
@@ -28,17 +49,10 @@
 *** Changes to Proof General RPM packaging mechanism
   
      Can now build RPM packages with "rpm -ta" from tarball source.
-     RPM includes menu file and icons (tested under Linux Mandrake).
+     RPM includes menu file and icons so that Proof General may
+     appear on your window system menus (tested under Linux Mandrake).
      We no longer distribute an SRPM.
 
-*** Command to insert last output as comment in proof script.
-
-     Sometimes it is useful to paste some of the output from
-     goals or response buffer into the proof script.  A new
-     function `pg-insert-last-output-as-comment' (C-c C-;)
-     inserts the last output and converts it into a comment
-     using `comment-region'.
-
 *** Compatibility fixes.
 
      Fixes for FSF Emacs and XEmacs 21.4
diff --git a/TODO b/TODO
index 4355d923..f163c797 100644
--- a/TODO
+++ b/TODO
@@ -14,7 +14,6 @@ proofgen@dcs.ed.ac.uk.  Thanks!
 Plans for upcoming versions
 ---------------------------
 
-
 * Support more proof assistants
 
 * Add a browser mode for browsing script files 
@@ -23,6 +22,12 @@ Plans for upcoming versions
 * More flexible goals buffer mode to allow menus of
   common proof commands.
 
+* Unified context (right-button) menu in and out of spans.
+  Including paste option and other editing commands.
+
+* Implement ideas in the Proof General White Paper. 
+  (See the Development section of the web page for a link).
+
 * A more flexible way of choosing which instance of PG we want,
   allowing matches on the buffer before choosing the mode function.
 
@@ -43,8 +48,5 @@ Plans for upcoming versions
   of proof assistants.  Alternative is to base markup of 
   undoable regions on proof assistant output or messages.
 
-* Implement ideas in the Proof General White Paper. 
-  (See the Development section of the web page for a link).
-
 * Make an XEmacs package