-*- outline -*-

* Summary of Changes for Proof General 3.2 from 3.1

----- NB: this is a pre-release of PG 3.2.  Bugs likely, please report ------ 



** 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.
  Fix to previous function (used by FSF Emacs) by Markus Wenzel.
  XEmacs uses new functions which have slightly different 
  behaviour.  If this is problematical, please report, and
  force the use of the old function by writing:

     (defalias 'proof-segment-up-to 'proof-segment-up-to-old)
 
  in your .emacs file. (Warning: only during pre-release!)

*** 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 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

  Please let me know of any cases where this fails.  

*** 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".

*** Improved behaviour of electric terminator

*** Quick menu option to select proof-follow-mode

*** 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  (C-c C-.)

*** Added possibility (internal) for switching prover's output on/off.

  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

*** More decoration of Coq output, uses CoqResp mode now

** LEGO Changes

*** Slight change in output during proof: shows final discharge messages

 This is a side effect of code rationalization in PG elsewhere.

** 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.

** Changes for developers to note

*** Rearrangement of elisp files and loading mechanism.
    
      Autoloads in proof-autoloads.el are generated from
      ;;;###autoload comments with `make devel.autoloads'

      Several new files, to "modularize" the code a bit more.

*** New mechanism for defining customizations per prover

      See Section 9 of proof-config.el.  New macros mean that we can
      write for example `proof-defasscustom web-page' to automatically get 
      `isa-webpage', `hol-webpage', etc, declared on loading.
      
      Proof assistant specific code can then just set/use these
      variables, without needing to set `proof-assistant-webpage' from
      `isa-webpage' etc.

      This slightly breaks the original pseudo object-oriented idea
      behind the instantiation mechanism (overriding methods, setting
      attributes) but works much more smoothly with customization.

*** Changed buffer mode name: pbp-mode -> proof-goals-mode, for uniformity.

*** Removed proof-terminal-string to simplify command setting

  [ONGOING]
  As a simplification of the code, and to allow possibility of
  PAs without a terminal string, more smoothly.
  It is now the responsibility of each proof assistant's customization
  to add proof-terminal-string to commands where necessary.  

*** New parsing mechanism in testing

  To allow more flexible proof script syntax for new provers.  
  Also efficiency improvements.
  This change results in a few known oddities at the moment, e.g. 
  process whole buffer leaves off last line.  
  Also broken with FSF Emacs.
  To test it, do 
    (defalias 'proof-segment-up-to 'proof-segment-up-to-new)

*** Other minor things (interest only to independent developers of PG modes):

      No need for match string 1 in proof-shell-proof-completed
      Added proof-shell-pre-sync-init-cmd, see doc.