-*- outline -*-

---   This is a development release of Proof General,     ---
---   some features may be incomplete or buggy.  Please   ---
---   report any problems to support@proofgeneral.org,    ---
---   thanks.  Check files BUGS and <prover>/BUGS first.  ---


* Summary of Changes for Proof General 3.5pre from 3.4

** Generic changes

*** IN PROGRESS:  pre-compiled .elc files: recompile needed for GNU Emacs

Proof General can now be reliably run as compiled code.

>>> Please help remove final difficulties by reporting problems <<<<

However, compiled Emacs Lisp files sometimes have incompatibilities
between versions (and definitely between GNU Emacs and XEmacs).  To
recompile the sources for a particular Emacs version, try:

  make clean
  make compile
 
Check the settings in the Makefile for your Emacs version.

*** Bundling of X-Symbol Mode (4.5 beta)

!!THIS IS WORK IN PROGRESS, IT MAY WELL BREAK X-SYMBOL FOR YOU!!

[ Currenly should be working in Isabelle, not other provers ]

To disable use of the bundled version, either delete/move away the
x-symbol subdirectory, or load your own local version first [put
(require 'x-symbol-hooks) in .emacs, or unpack in your own .xemacs
directory].

From now on, PG is not backward compatible with previous X-Symbol
versions.  Either upgrade your installed version, or be careful to
load PG first (so that the bundled version of X-Symbol is used).

Notice that the package version of X-Symbol may load itself first by
default during XEmacs startup, so it may be tricky to override.  If in
doubt, run with "xemacs -no-site-file -q" first.

*** Bundling of MMM Mode (for multiple modes in one buffer)

MMM mode allows submodes to be used in the same file.
See http://mmm-mode.sourceforge.net/.
At present it is configured for Isar, to allow LaTeX and sml-mode to
be used inside Isar scripts.  Contributions of configuration for other
provers welcomed.

*** X-Symbol (and MMM-mode) minor mode behaviour simplified
 
These minor modes like to be responsible for turning themselves on and
off.  PG does not anymore try to synchronise the on/off settings in
all PG buffers (which could lead to half an hour of fontification!).
Instead the menu reflects the current minor mode status; toggling it
will also update the default "global for PG" behaviour for new script
buffers.

*** Strict read only added to Proof General -> Options menu

Strict read only behaviour for the locked (blue) region
can now be enabled/disabled without restarting scripting.
(Output hightlighting option has been removed from this menu,
but is still available under 
   Advanced -> Customize -> User Options -> ..

*** Follow mode: add "followdown" setting

In this mode, the point moves with the locked region when it moves
down in the buffer (processing).  For undo, the point does not move.

*** Options and proof assistant settings improvements

Facility to reset to default values added, and saving
of (just) proof assistant settings.

*** Display management: added shrink-windows-tofit option

Attempt to shrink output windows to fit their contents in case it is
less than 1/2 the window height.  In progress; occasional flaws
(e.g. when output window buffer total window height).  Available
under PG -> Options -> Display -> Shrink To Fit.

*** Add proof-indent-pad-eol setting to prettify locked regions in XEmacs.

*** Parsing internals changed: minor user visible differences

Please report any problems/annoyances which may be unexpected.
NB: Not yet enabled for Isabelle/Isar.

*** Tweaks to menus,  colours

Electric terminator menu option more visible. 
Reduce contrast for mouse highlighting of regions.


** GNU Emacs compatibility, simplified font-lock, handling nested comments

*** Numerous improvements, thanks due to Stefan Monnier.

*** Some GNU Emacs backwards compatibility removed: use 21.1 or later

*** PROBLEMS REMAINING: Menu problems currently on 21.2, may affect loading.
    Temp fix: turn on mode manually first in *scratch* buffer, then
    visit file.

** Changes for Isabelle

Beginnings of support PGIP protocol (work in progress with Isabelle
2003).  Presently allows Isabelle to configure Proof General prover
settings menu.

Backward compatibility may not be maintained: it's simply too much
effort.  This means that if you upgrade your Emacs version, which
forces you to upgrade Proof General because Emacs upgrades usually
break Proof General (Emacs authors pay little heed to maintaining
APIs), then you may have to upgrade your Isabelle version as well.