Add support for Imenu. Fix other bits here.

1 files changed, 24 insertions, 17 deletions

diff --git a/CHANGES b/CHANGES
index 664b4b07..c78747a3 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,14 +1,25 @@
 -*- outline -*-
 
----   This is a development release of Proof General,      ---
----   some features may be incomplete or buggy.  Please    ---
----   report any problems to da+pg-support@inf.ed.ac.uk    ---
----   thanks.  Check files BUGS and <prover>/BUGS first.   ---
+* Summary of Changes for Proof General 3.5 from 3.4
 
+** Generic changes
 
-* Summary of Changes for Proof General 3.5pre from 3.4
+*** Support for Speedbar and Index menu ("Imenu")
 
-** Generic changes
+Imenu is an alternative to Function Menu (which is described in the
+Proof General manual).  It displays a menu of named definitions,
+theorems, etc, in the file and allows quick navigation to them.
+
+Speedbar displays a file tree in a separate window on the display,
+allowing quick navigation.  Middle/double-clicking or pressing + on a
+file icon opens up to display tags (definitions, theorems, etc) within
+the file.  Middle/double-clicking on a file or tag jumps to that file/tag.
+
+To use Imenu, select Proof General -> Options -> Index Menu.
+
+To use Speedbar, use Tools -> Display Speedbar (GNU Emacs), or
+Proof General -> Advanced -> Speedbar (XEmacs).  Or if you prefer
+the old fashioned way, `M-x speedbar' does the same job.
 
 *** Improved display management
 
@@ -33,10 +44,8 @@ Please try out these packages and report any problems.
 *** Desktop integration on freedesktop.org compliant desktops
 
 Provided automatically (and only) with the RPM package.
-
-WORK IN PROGRESS!!  -- Please send me i18n strings, and report
-  any problems on particular desktops 
-  (I'm only testing on Fedora Core 1/GNOME).
+Please send in i18n strings, and report any problems on particular
+desktops (only tested on Fedora Core 1/GNOME).
 
 *** Keyboard hints and other messages displayed in minibuffer
 
@@ -44,12 +53,10 @@ Hints for keyboard usage and reporting on file processing are now
 displayed in the minibuffer.  If you do not like this behaviour,
 customize the `pg-show-hints' variable.
 
-*** pre-compiled .elc files: recompile needed for GNU Emacs
+*** pre-compiled .elc files: NOTE recompile needed for GNU Emacs
 
 Proof General can now be reliably run as compiled code.
 
->>> Please help remove any final difficulties by reporting problems <<<<
-
 However, compiled Emacs Lisp files sometimes have incompatibilities
 between versions (and definitely between GNU Emacs and XEmacs).  To
 recompile the sources for a particular Emacs version, try:
@@ -61,10 +68,6 @@ Check the settings in the Makefile for your Emacs version.
 
 *** Bundling of X-Symbol Mode (4.5.1-beta)
 
-!!THIS IS WORK IN PROGRESS, IT MAY WELL BREAK X-SYMBOL FOR YOU!!
-
-[ Currently should be working in Isabelle, perhaps not other provers ]
-
 To disable use of the bundled version, either delete/move away the
 x-symbol subdirectory, or load your own local version first [put
 (require 'x-symbol-hooks) in .emacs, or unpack in your own .xemacs
@@ -105,6 +108,10 @@ By default, the cursor jumps to the end of the locked region on an
 error.  Previously it also jumped on an interrupt.  This is configurable
 via `proof-shell-handle-error-or-interrupt-hook', which see.
 
+After an interrupt you may use C-c . to move to the end of the
+locked region, or C-c ` (backquote) to move to the location 
+given by an error message from the prover.  
+
 *** Automatic slow-down on fast tracing display
 
 Proof General will try to configure itself to update the display of