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

*** Makefile has new target "scripts" to fix 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.]

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

*** Favourites: user-defined commands added proof assistant specific menu

  WORK ONGOING: PRESENTLY INCOMPLETE, DO NOT REPORT!

*** Menu reorganization, including new proof assistant specific menus.  

  Specific menus added for Coq, LEGO, Isabelle.

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

*** Efficiency improvement in parsing
 
  Also works around crash bug in xemacs-21.1.7/SuSE.
  Fix by Markus Wenzel.

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

  Already implemented in Coq and Isabelle(/Isar).


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