From 5cdc85afc18a2056649b680688d00ea6b11db256 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 29 Aug 2002 16:29:47 +0000 Subject: Changes for development release --- CHANGES | 150 +++------------------------------------------------------------- 1 file changed, 6 insertions(+), 144 deletions(-) diff --git a/CHANGES b/CHANGES index ebece014..e9a47964 100644 --- a/CHANGES +++ b/CHANGES @@ -1,151 +1,13 @@ -*- outline -*- -* Summary of Changes for Proof General 3.4 from 3.3 +--- 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 /BUGS first. --- -** Generic Changes -*** LICENSE CHANGE to GPL! +* Summary of Changes for Proof General 3.5pre from 3.4 -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 + << No changes yet >> -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. - -*** Desktop integration for RedHat 7.3, Mandrake 8.2 in RPM package. - -RPM package now works on RedHat as well as Mandrake, and adds PG application -to desktop menus. - -*** Efficiency improvements - -Process buffers no longer keep undo information. - - - -** 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. -- cgit v1.2.3