Merge changes from Version4Branch.

1 files changed, 6 insertions, 507 deletions

diff --git a/CHANGES b/CHANGES
index 85b5db98..9fff26cf 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,515 +1,14 @@
 -*- outline -*-  
 
-* Summary of Changes for Proof General 3.7.1 from 3.7
+* Summary of Changes for Proof General 4.0 from 3.7.X
 
 ** Generic changes
 
-*** Fixes and improvements, compatibility patches
+*** XEmacs is no longer supported; PG only works with GNU Emacs 22.2+
 
-- 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.
+*** Font-lock based Unicode Tokens mode replaces X-Symbol
 
-** Isabelle changes
+*** X-Symbol is no longer used or bundled
 
-- 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.
+*** Removed configuration options
+    proof-toolbar-use-button-enablers  (now always enabled)