-*- outline -*-

* Summary of Changes for Proof General 3.4 from 3.3

** Generic Changes

*** LICENSE CHANGE to GPL!

It is now permitted to use Proof General in any context, without
applying for a special license from University of Edinburgh.  
Free redistribution is also allowed under the GPL conditions.

*** Support added for GNU Emacs 21.X; no support for GNU Emacs 20.X

Toolbar, splash screen, and X-Symbol are all supported in GNU Emacs.  

Sorry, this version of PG does not support Emacs 20; backwards
compatibility is far too difficult to maintain.

*** Colours altered

Colours made a little less lurid.  Reverse video tweaks.
(Look in proof-config for proof-locked-face, proof-queue-face
and old settings if you want to change back: 
use M-x customize-face, M-x list-faces-display, 
M-x list-colours-display to play with your own defaults).

*** Improvements to visibility controls

Visibility controls now work for comments as well as proofs in
proof scripts.  An image is used in XEmacs to signal hidden text.

*** Context-sensitive menu (right mouse) now has additional features

The context sensitive menu for regions of the buffer which have
been processed allows several features, including hiding/revealing
the area, copying it, and some prover-specific commands -- in
Isabelle you can ask for a graph of the theorem dependencies (thm_deps),
in Coq you can ask for the proof term to be printed.  
(Please send us suggestions for other useful features here).

*** Menu improvements (favourites, options saving)

Favourites are now more robust.  You can delete them and save them
when you want.  The PG "quick" options can also be saved separately
from other Emacs custom variables.

*** Support for "tracing" buffers improved and enabled by default.

(Tracing is only deployed in Isabelle so far)
Compared with experimental tracing in PG 3.3, there is now only one
tracing buffer, treated somewhat like a response buffer.
For minor issues, see isa/BUGS.

*** Easily remove handling for provers you don't want 

You can simply remove the directories from the PG distribution,
instead of customizing the `proof-assistants' variable.

*** Various efficiency improvements 


*** Desktop integration for RedHat 7.3, Mandrake 8.2 in RPM package.




** Isabelle Changes

*** Isabelle/Isar syntax changes, other tweaks for Isabelle2002.

Switch to using Isabelle/Isar by default for .thy files.
Support next error function.

Isabelle classic mode: highlighting tweaks for ML code contributed by
Lucas Dixon (lucasd@dai.ed.ac.uk)

*** Active highlighting of variables  [ EXPERIMENTAL FEATURE: see README.exper ]

Variables are made active in the goals buffer.  Hovering the mouse
over an identifier shows its type.  

This handy feature is a glimpse of what could be done with proper
subterm markup, which needs support to be added in the Isabelle core.


** Coq Changes

*** Much improved synchronization of PG/Coq. 

Commands like Hint, Require, etc, were not backtracked correctly, but
are now. Nested proofs and commands nested in proofs are now also well
backtracked.

User defined keywords could not completely well backtracked. The
fall-back mechanism is better now, but to solve this completely we
provide four configurable variables for registering personal tactics
and commands. Commands and tactics are split into state-preserving or
state-changing commands and tactics, i.e. which need or not Back/Undo
to be backtracked. This allows PG to
1) (more important) to correctly backtrack user-defined commands and
   tactics.
2) colorize correctly 

See `coq-user-state-preserving-commands, `coq-user-state-changing-commands,
`coq-user-state-preserving-tactics, `coq-user-state-changing-tactics'

These variables are regexp lists. See their documentations in emacs of
this variable (C-h v coq-user...) and in the doc, for details on how
to set them in your .emacs file.  Example:

 An example of existing commands that fit each category:

   coq-user-state-preserving-commands: example: "Print"

   coq-user-state-changing-commands:     example: "Require"

   coq-user-state-changing-tactics:      example: "Intro"

   coq-user-state-preserving-tactics:  example: "Proof"

   This variables are string lists. See the documentations in emacs of
   this variable (C-h v coq-user...)  for details on how to set them
   in your .emacs file.

   Example:
   (setq coq-user-state-changing-commands 
	  '("MyHint" "MyRequire" "Show\\-+Mydata"))

	Last thing: you must restart emacs to allow emacs take these
	variable into account.


** Changes for other provers

*** ACL2 improved (now issues undo commands)
Still experimental and in need of official support.


** Changes for proof assistant developers to note
  
*** Improvements in instantiation mechanism

Allow smoother support for provers which only use scripting, and do
not make use of goals window (e.g. Twelf, ACL2).  We no longer warn if
inessential settings like proof-goal-command and similar are unset,
but instead automatically remove toolbar and menu items
correspondingly.