-*- outline -*-  

* Summary of Changes for Proof General 3.7.1 from 3.7

** Generic changes

*** Fixes and improvements, compatibility patches

- Unicode Tokens: supports control tokens (Isabelle sub/super/fonts).
   This is experimental; editing files with subs/supers may be unreliable.
   X-Symbol is still recommended.  Please note: this mode will
   probably be dropped in future, in favour of a font-lock based
   mechanism more similar to X-Symbol.
- Fix Options saving for MMM, Maths Menu, Unicode Tokens.
- Compatibility improvements for: Carbon Emacs, latest Emacs 23 CVS.

** Isabelle changes

- Choice of isabelle command command based on isatool, if run outside wrapper
- Logic can be set in comment: (* -*- isabelle-chosen-logic: "ZF" -*- *)

** Coq changes

- Add Undo Depth setting, default to 200 (Coq 8.1 has only 100)
- Unicode error messages are correctly highlighted with emacs23
  (emacs-snapshot), previous emacs's can't be fixed.


* Summary of Changes for Proof General 3.7 from 3.5  (via 3.6pre)

** Generic changes

*** Fixes and additions, patches for recent Emacs versions

- Improved display of X-Symbol subscript/superscripts in GNU Emacs 22.1.
- Workarounds for bugs in XEmacs 21.5 beta (but GNU Emacs now preferred).
- Reworked icons to better match style of GNU Emacs/Gnome.
- History for processed commands in active script buffer (M-n, M-p)
- Undo history in read-only area discarded (see: proof-allow-undo-in-read-only)
- Context menu for spans: option to undo.
- proof-indent-pad-eol option removed (spurious spaces were objectionable)
- Many fixes and code cleanups.

*** X-Symbol support on native Mac Emacs

This works for Carbon Emacs version of GNU Emacs 22.X, using 
Norbert Voelker's TrueType version of the X-Symbol1 font.
See x-symbol/README.x-symbol-for-ProofGeneral

*** New input mechanisms for Unicode added (preliminary version)

Maths Menu (by Dave Love) for inserting Unicode math characters.
GNU Emacs only.

Unicode Tokens mode, an experimental X-Symbol replacement, for
displaying ASCII tokens as Unicode strings (for Isabelle) and
providing shortcut input for Unicode sequences (for Isabelle, Coq).
Much simpler than X-Symbol, but requires a suitably rich Unicode font.
GNU Emacs >=23 recommended but works elsewhere.  

Try Options -> Set Fontset to find a good font (e.g. "standard").
Customize the tables with 

  M-x customize-variable isar-token-name-alist
  M-x customize-variable isar-shortcut-alist

or edit isar/isar-unicode-tokens.el.  Similarly for Coq.
Symbol rotation (next/previous glyph) on C-, and C-.  (GE>=23)



*** UTF-8 support for 8-bit clean provers

Support for Unicode-safe interaction modes has been added (i.e., not
using Unicode-prefix characters as special escape sequences).  See
proof-shell-unicode (default t), or option -U of the Isabelle 
interface wrapper.

*** Large X-Symbol fonts added, courtesy of Clemens Ballarin

Use option -f 18 or -f 24 of the Isabelle interface wrapper.



** Changes for Isabelle

*** Support for Isabelle2005 and Isabelle2007.

Menu functions now controlled directly by Isabelle.  Support for
Unicode-safe interaction (`proof-shell-unicode' variable).

Support for Isabelle2003 and Isabelle 2004 removed.
Code works with PolyML 5 versions of Isabelle.

Optional search form for the "Find Theorems" command is available via
C-c C-a C-f, the minibuffer interface is available via C-c C-a C-m.
Variable proof-find-theorems-command (customizable via 'Proof-General
-> Advanced -> Internals -> Prover Config') controls the default
behavior of 'ProofGeneral -> Find Theorems' (C-c C-f): set to
isar-find-theorems-form or isar-find-theorems-minibuffer.



** Changes for Coq

*** No more support for coq 7.x

*** Support for ssreflect proof mode
Support added by Assia Mahboubi.

*** coq 8.0 compatibility mode

If coq does not detect the good coq version at startup put one of
the following in your .emacs:

(setq coq-version-is-V8-1 t)   or    (setq coq-version-is-V8-0 t)

Default is now 8.1 (if no coqtop is found the path).

*** Much better PG/Coq synchronizing system for coq >= 8.1

    Synchronization is not based on script parsing anymore, which
    makes it much more reliable. 

    In particular you don't need to set
    coq-user-state-changing-commands and others anymore (was needed
    for your own tactics/commands). See below coq-insert-tactic.

    Coq v8.0 is still supported, if for some reason PG does not see
    that your coq version is a 8.0 (read *Message* after loading a .v
    file), then set variable coq-version-is-V8-0 to t in your emacs
    init file. Otherwise PG will hang at first line when scripting.

*** error highlighting

    When scripting, error with location information are parsed and the
    corresponding part of the scripting buffer is highlighted. Also
    inpsired from coqide.

*** Much better indentation

    More robust. Nested comments are OK even in xemacs. Still a bit
    slow on big files. 

    indent-region won't touch comments, but indenting comments with
    tab (indent-according-to-mode) will.

*** new coq-insert-tactic and coq-insert-command function

    These two functions allow to insert a tactic or command with
    completion in the mini-buffer.

*** New variables coq-user-commands-db, coq-user-keywords, coq-user-tactics-db

    User defined tactics/commands information.  See C-h v
    coq-syntax-db for syntax. It is not necessary to add your own
    tactics here if you have coq v8.1 (it is not needed by the
    synchronizing/backtracking system). You may however do so for the
    following reasons:

    1 your tactics/commands/keyword will be colorized by font-lock

    2 your tactics/commands will be added to the menu and to completion
    when calling coq-insert-tactic/command (see below)

    3 you may define an abbreviation for your tactic/command.

    The file coq/ex-ssreflect.v contains an example of such
    customization, together with a coloured script containing
    user-defined tactics/commands/keywords.

*** automatic insertion of "match...with" for a given type

    This coqide great feature has been added.

*** Local Variables List semi automatic filling

    Local Variables Lists are used to set coq program name and arguments
    persistently for a given file. The menu entry "set coq prog
    persistently" helps you to define or change the values in this list
    (which are store as a comment at the end of the file, see info
    manual at node ((emacs)File Variables).

*** Better font-lock coloration

*** new "queries" menu

*** Adapted error highlighting to x-symbol

*** Response windows shrinking to fit in three window mode

*** Outline mode cleaner




* Summary of Changes for Proof General 3.5 from 3.4

** Generic changes

*** Support for Speedbar and Index menu ("Imenu")

Imenu is an alternative to Function Menu (which has been supported for
some time, but is not built-in to GNU Emacs).  It displays a menu of
named definitions, theorems, etc, in the file and allows quick
navigation to them.

Speedbar displays a file tree in a separate window on the display,
allowing quick navigation.  Middle/double-clicking or pressing + on a
file icon opens up to display tags (definitions, theorems, etc) within
the file.  Middle/double-clicking on a file or tag jumps to that file/tag.

To use Imenu, select Proof General -> Options -> Index Menu.  This adds
an "Index" menu to the main menu bar.  You can also use M-x imenu for
keyboard-driven completion.

To use Speedbar, use Tools -> Display Speedbar (GNU Emacs), or
Proof General -> Advanced -> Speedbar (XEmacs).  Or if you prefer
the old fashioned way, `M-x speedbar' does the same job.

For more about Speedbar, see http://cedet.sourceforge.net/speedbar.shtml

*** Improved display management

The display handling functions have been overhauled to cope with
latest API changes and diversions between Emacs versions.  Multiframe
mode should now work reasonably well on both Emacs versions, with
cut-down frames (no toolbars, etc).  There is a new user-level
function `proof-layout-windows' which displays windows in a default
form for the current display mode.  This uses a vertical-horizontal
split scheme for three-pane mode (due to Pierre Courtieu), but
three-pane mode also works with three-way horizontal split as before.
See note in BUGS for remaining issues.

*** More example proofs included

Some additional example proofs are included with this release (and we
hope to add more).  The best and most accurate resource is of course
the distribution of each proof assistant, but including some samples
in Proof General allows you to see proofs in other systems without
having to install them all.

The "root2" example proofs of the irrationality of the square root of
2 were proofs written as a response to a challenge of Freek Wiedijk in
his comparison of different theorem provers, see
http://www.cs.kun.nl/~freek/comparison/.  Those proof scripts are
copyright by their named authors or as mentioned in the files.


*** Improved RPM packages

Three packages are provided: ProofGeneral, ProofGeneral-emacs-elc and
ProofGeneral-xemacs-elc.  The two elc RPMs contain compiled elisp for
GNU Emacs and XEmacs respectively.  These RPMs are intended to be
compatible with the RPMs distributed with Red Hat/Fedora. 

Please try out these packages and report any problems.

*** Desktop integration on freedesktop.org compliant desktops

Provided automatically (and only) with the RPM package.
Please send in i18n strings, and report any problems on particular
desktops (only tested on Fedora Core 1/GNOME).

*** Keyboard hints and other messages displayed in minibuffer

Hints for keyboard usage and reporting on file processing are now
displayed in the minibuffer.  If you do not like this behaviour,
customize the `pg-show-hints' variable.

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

Proof General can now be reliably run as compiled code.

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.1-beta)

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 (especially if you have it installed
site-wide), so it may be tricky to override.  You can prevent this
with "xemacs -no-autoloads", but that may result in other needed
packages not being loaded!  There is an attempt to prevent the
built-in version loading in Proof General, but in case of problems,
consult your sysadmin to try to prevent global loading of x-symbol.

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

*** Movement of cursor on interrupt is disabled

By default, the cursor jumps to the end of the locked region on an
error.  Previously it also jumped on an interrupt.  This is configurable
via `proof-shell-handle-error-or-interrupt-hook', which see.

After an interrupt you may use C-c . to move to the end of the
locked region, or C-c ` (backquote) to move to the location 
given by an error message from the prover.  

*** Automatic slow-down on fast tracing display

Proof General will try to configure itself to update the display of
tracing output infrequently when the prover is producing rapid,
perhaps voluminous, output.  This counteracts the situation that
otherwise Emacs may consume more CPU than the proof assistant, trying
to fontify and refresh the display as fast as output appears.
See `proof-trace-output-slow-catchup' for setting.


*** Proof General -> Options menu changes

**** Improvement to options handling

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

**** Strict read only added

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

**** Deactivate Action added 

This setting controls an automatic action when scripting is
deactivated in a partially processed buffer.  Ordinarily, PG will
query whether to retract or completely process the file.
One of these can be chosen as a default action.

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

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

This option shrinks and expands the display of prover output,
within reasonable window sizes, when in 2-window mode.  It avoids
wasting half the screen with empty space (with the drawback
of moving the boundary up and down).

Available under PG -> Options -> Display -> Shrink To Fit.

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

This works by adding unnecessary spaces to the end of lines when TAB
is pressed.

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

*** Added `proof-shell-identifier-under-mouse-cmd'

Allows PG to conveniently send a command to the prover which passes
the identifier under the mouse, or the active region, as an argument.
Bound globally to Control-Meta-Mouse-button1.

Presently only configured in Isabelle/Isar, to parse terms (inside
strings) and theorems (outside).


** New "experimental" features

These are only available if `proof-experimental-features' is
customized to t.

*** "Move up" and "Move down" functions in context span menu 
   (use right-click on highlighted spans), also bound on
   C-M-up/C-M-down.

*** Theorem dependencies: displaying and highlighting dependencies.
   Dependencies (e.g. lemmas) for a theorem are highlighted in 
   yellow, places where the theorem is used are highlighted
   in orange.   This allows easy editing of theories to remove
   dead lemmas, re-order proofs, etc.

   This only works in Isabelle at the moment.  (Support is required
   from other proof assistant authors: please suggest to them!).  You
   must select the Isabelle setting "Theorem Dependencies" before
   starting Isabelle, to enable gathering of data.

*** Active highlighting for variables in Isabelle.
   Moving the mouse over variables in the goal display will display
   some information.  The information in Isabelle/Isar is the type of
   the variable, often, but it depends on the context and may be
   wrong.  In Isabelle/classic the type information is useless.
   This feature is a vague hint of what could be done with proper subterm
   markup from the Isabelle engine.  Without this, it cannot work
   well, because no context is available for Proof General to send
   back to the prover, so only variables bound at the outer level can 
   have sensible information displayed, via the "term" command.





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

** Changes for Isabelle

*** Automatic refreshing of Logics list

*** Theorem dependencies: displaying and highlighting dependencies.

Dependencies for a theorem (i.e. other theorems,lemmas) can be
displayed.  Local dependencies within the same file can be highlighted
in yellow, and places where a theorem is used are highlighted in
orange.  This aids editing of theories to remove dead lemmas, re-order
proofs, etc.  To activate it you need to select the "Theorem
Dependencies" option in the Isabelle(/Isar) -> Settings menu.  

You may need to restart the prover before doing this to gather full
dependency information.

*** Beginnings of support PGIP protocol (wip with Isabelle2004)  

This is an internal change.  Presently, it allows Isabelle to
configure Proof General prover settings menu directly rather 
than using Elisp.


** Changes for Coq

*** Coq 8.0 compatibility.  Example files are Coq 8.0 format.

**** Possibility to run Coq 8.0 in compatibility mode
**** Further prover settings added
**** Automatic compilation ("auto-compile-vos"), dependencies managed

*** Command coq-intros inserts intros using "Show Intros" output

*** Indentation improved

*** Menu entries for inserting commands, tactics and terms

*** "Holes" system, for editing structured expressions

Holes are a powerful feature for complex expression editing. It is
inspired from other tools, like Pcoq
(http://www-sop.inria.fr/lemme/pcoq/index.html). The principle is
simple, holes are pieces of text that can be "filled" by different
means. The new menu system makes use of the holes system. Almost all
holes operations are available in the Coq/holes menu.

Note: Holes and menus make use of emacs abbreviation mechanism, please
make sure you don't have an abbrev table defined in you config files
(C-h v abbrev-file-name to see the name of the abbreviation file). If
there is already such a table, you can do the following to merge with
ProofGeneral's abbrev: M-x read-abbrev-file, then find the file named
"coq-abbrev.el" in the ProofGeneral/coq directory. At emacs exit you
will be asked if you want to save abbrevs, answer yes.

*** X-symbols are much improved (more symbols, cleaner grammar)

Much more symbols are supported now (C-= C-= for the symbol table).
See coq/README for more details, including the syntax of sub/superscripts.

** Additional instances of Proof General

*** ccc:  Proof General for the Casl Consistency Checker

Provided by Christoph Lüth <cxl@informatik.uni-bremen.de>.
See http://www.informatik.uni-bremen.de/cofi/ccc for more information.

*** pgshell:  Proof General for shell scripts/simple command interpreters.

This instance of PG is handy just for using script management to
cut-and-paste into a buffer running an ordinary shell or tool
with a command-line interpreter of some kind.  

Provides an instant and cheap interface to command-line interpreters,
to avoid tiresomely using cut-and-paste to run pre-recorded commands.
