-*- outline -*-

* Summary of Changes for Proof General 3.1 from 3.0


** New instantiations of Proof General!

*** HOL 98 (http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html)

   by David Aspinall.  This is a bare-bones Proof General instance
   only, hopefully to entice HOL users so that someone may improve it.
   See README in the hol98 directory for more details.

*** Plastic (http://www.dur.ac.uk/CARG/plastic.html)
  
   by Paul Callaghan <P.C.Callaghan@durham.ac.uk>.
   The Plastic system itself is not yet publicly available,
   so this is only included in the developers tar file.


** Generic Changes

*** README file added for each supported prover, explaining support.

*** Fixes for supporting Japanese versions of Emacs which have older CL macs.
 
  Probs with CL macs with Japanicised documentation, defined in "egg.el".
  Japanese Emacs users, please report any other problems you find, they 
  may be fixable for similar reasons.

*** Minor bug fix for duplicated short output.
  
  Only seen with "val x=1" or similar messages.
  We now set proof-shell-eager-annotation-start-length appropriately.

*** Bug fix with .thy files and X-Symbol mode
  
  Subsequently visited theory files would have X-Symbols broken.  

*** Bug fix for (non-mule) FSF Emacs 20.5.  

  Emacs would freeze when starting proof assistant due to character 
  matching problem.

*** Fix for infamous Solaris ^G problem: proof-shell-process-connection-type 

  A user (or proof assistant configuration) can now specify whether
  to use pty or piped communication.  This is to fix the problem that
  Solaris users have (because of a Solaris bug), when lots of ^G's
  appear.  
  
  The default setting for proof-shell-process-connection-type is made
  by examining the ARCH environment variable.  If this contains "sun"
  then proof-shell-process-connection-type is set to nil for using
  pipes.  Otherwise we use ptys which are to be prefered over pipes
  because pipes can become full or lose data, and pipes don't work
  which some proof assistants.

  If necessary, you can override this by customization, as usual.
  
*** Added new configuration hook:  proof-shell-pre-interrupt-hook

  This is 

** Coq Changes


** LEGO Changes

*** Fix for error messages, now properly displays "cannot assume" message.


** Isabelle Changes

***


** Isar Changes

*** Minor syntax tweaks.


** Changes for developers to note

*** todo file added for each prover, split from global todo file