From 600bc120f3c8c17d5682c5b06255e0b6706d1201 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 14 Apr 2004 13:05:34 +0000 Subject: Add support for Imenu. Fix other bits here. --- CHANGES | 41 ++++++++++++++++++++++++----------------- 1 file changed, 24 insertions(+), 17 deletions(-) (limited to 'CHANGES') 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 /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 -- cgit v1.2.3