proof-next-error, proof-display-some-buffers

1 files changed, 25 insertions, 13 deletions

diff --git a/CHANGES b/CHANGES
index c1cff785..83f47f75 100644
--- a/CHANGES
+++ b/CHANGES
@@ -8,6 +8,14 @@
 
 ** Generic Changes
 
+*** Added proof-next-error function, bound to C-c `
+
+  When the proof assistant batch loads files "in the background"
+  rather than incrementally via script management, error messages
+  may appear in the response buffer with file/line numbers.
+  Proof General can now parse these messages to jump to the
+  location of the error.
+
 *** New more efficient and generalised parsing functions
  
   Also works around crash bug in xemacs-21.1.7/SuSE.
@@ -20,18 +28,18 @@
  
   in your .emacs file. (Warning: only during pre-release!)
 
-*** Makefile has new target "scripts" to fix paths in bash/perl scripts
+*** Makefile has new target "scripts" to adjust paths in bash/perl scripts
 
 *** Bug fix: "next" button enabled more often.  Solaris turns off enablers.
 
 *** Bug fix: first line ignored problem fixed for Coq and others.
  
   To fix this properly, we have added `proof-shell-pre-sync-init-cmd'
-  for provers need initialization before synchronization can be secured.
-  [Developers note: LEGO needs to wait for second prompt before sync,
-   whereas Isabelle managed to sync on first prompt.  Coq was best,
-   with sync set before startup, using a command line option.
-   That is the recommended route for new proof assistants.]
+  for provers that need initialization before synchronization can be
+  secured.  [Developers note: LEGO needs to wait for second prompt
+  before sync, whereas Isabelle managed to sync on first prompt.  
+  Coq was best, with sync set before startup, using a command line option.
+  That is the recommended route for new proof assistants.]
 
 *** Bug fix: script management is now more robust against C-x C-v, C-x C-w
 
@@ -39,12 +47,10 @@
 
 *** Menu reorganization, including new proof assistant specific menus.  
 
-*** Favourites: user-defined commands added proof assistant specific menu
-
-*** Menu reorganization, including new proof assistant specific menus.  
-
   Specific menus added for Coq, LEGO, Isabelle.
 
+*** Favourites: user-defined commands added proof assistant specific menu
+
 *** Proof assistant specific keymap added
 
   Keybindings for proof assistant now begin with "C-c C-a".
@@ -57,11 +63,17 @@
 
   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.
+  using M-x proof-goto-end-of-locked  (C-c C-.)
 
-*** Added possibility for switching prover's output on/off.
+*** Added possibility (internal) for switching prover's output on/off.
 
-  Already implemented in Coq and Isabelle(/Isar).
+  Already implemented in Coq and Isabelle(/Isar).  
+  This improves efficiency by giving more CPU to prover.
+
+*** Added handy proof-display-some-buffers (C-c C-l)
+ 
+  This displays the response buffer (usually), or the goals buffer
+  as well if you are in three window or multiple frame mode.
 
 
 ** Coq Changes