-*- outline -*-

--- This is a development release of Proof General,   ---
--- some features may be incomplete or buggy.  Please ---
--- report any problems to da@dcs.ed.ac.uk, thanks.   ---
--- ID: $Id$	      			              ---

* Summary of Changes for Proof General 3.4pre 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.

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

*** Colours altered

Queue and locked colours made a little less lurid.
(Look in proof-config for proof-locked-face, proof-queue-face
and old settings if you want to change back).

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


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



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


** 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 are not completely well backtracked. To solve
this we provide customization, using four configurable variables for
registering personal tactics and commands. Commands and tactics are
split into backable (resp. undoable), i.e. which need "Back"
(resp. "Undo") to be backtracked and not backable (resp. not
undoable). This allows PG to 1) colorize correctly 2) (more important)
to correctly backtrack user-defined commands and tactics.

See `coq-user-non-backable-commands', `coq-user-backable-commands',
`coq-user-undoable-tactics', `coq-user-non-undoable-tactics'

These variables are regexp lists. See their 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-backable-commands 
	  '("MyHint" "MyRequire" "Show\\-+Mydata"))



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