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

*** Bug fix: "next" button enabled more often.  Solaris turns off enablers.

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

  Specific menus added for Coq, LEGO, Isabelle.

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

  WORK ONGOING: PRESENTLY INCOMPLETE, DO NOT REPORT!

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

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