From 1f813ce63369aa520d38e3152a1013d1f97c7024 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Sun, 15 Aug 2010 22:56:13 +0000 Subject: Update. --- CHANGES | 43 ++++++++++++++++++++++++++----------------- 1 file changed, 26 insertions(+), 17 deletions(-) (limited to 'CHANGES') diff --git a/CHANGES b/CHANGES index 9db1b930..9426317d 100644 --- a/CHANGES +++ b/CHANGES @@ -2,10 +2,17 @@ * Main Changes for Proof General 4.0 from 3.7.1 -** Generic changes +** Install/support changes *** XEmacs is no longer supported; PG only works with GNU Emacs 22.2+ +*** Primary distribution formats changed + The RPM and zip file formats have been removed. + We are very grateful to third-party packagers for Debian and Fedora + for distributing packaged versions of PG. + +** Generic changes + *** Font-lock based Unicode Tokens mode replaces X-Symbol Unicode Tokens has been significantly improved since PG 3.7.1, and now works purely at a "presentation" level without changing @@ -19,26 +26,24 @@ - ...but "sticky" colouring for errors can be used - edit on processed region can automatically undo - Depending on input language and interaction output, this may + Depending on the prover language and interaction output, this may enable a useful "document centred" way of working, when output - buffers can be ignored and hidden. - Use "full annotation" to keep output when several steps are taken. + buffers can be ignored and hidden. Use "full annotation" to keep + output when several steps are taken. -*** "Movie" output: export an annotated buffer in XML - Basic movie output for Proviola, see http://mws.cs.ru.nl/proviola +*** Automatic processing mode (experimental) + Quick Options -> Send Automatically + Sends commands to the prover when Emacs is idle for a while. + NB: EXPERIMENTAL this is in progress, currently too obtrusive + to be usable. *** Improved prevention of Undo in locked region With thanks to Erik Martin-Dorel and Stefan Monnier. Undo in read only region follows `proof-strict-read-only' and gives the user the chance to allow edits by retracting first. -*** Simplified version of comint now used for proof shell - To improve efficiency, a cut-down version of comint is now used. - Editing, history and decoration in the shell (*coq*, *isabelle*, - etc) are impoverished compared with PG 3.X. - *** Proof General -> Options menu extended and rearranged - - new menu for useful minor modes suggests modes that PG supports + - new menu for useful minor modes indicates modes that PG supports *** New user configuration options (also on Proof General -> Options) proof-colour-locked (use background colour for checked text) @@ -52,6 +57,9 @@ proof-toolbar-use-button-enablers (now always used) proof-output-fontify-enable (now always enabled) +*** "Movie" output: export an annotated buffer in XML + Basic movie output for Proviola, see http://mws.cs.ru.nl/proviola + *** Altered prover configuration settings (internal) urgent message matching is now anchored; configurations for @@ -69,16 +77,17 @@ proof-shell-error-or-interrupt-seen: removed, use p-s-last-output-kind proof-script-next-entity-regexps,next-entity-fn: removed (func-menu dead) -*** Primary distribution formats changed - The RPM and zip file formats have been removed. - We are very grateful to third-party packagers for Debian and Fedora - for distributing packaged versions of PG. +*** Simplified version of comint now used for proof shell (internal) + To improve efficiency, a cut-down version of comint is now used. + Editing, history and decoration in the shell (*coq*, *isabelle*, + etc) are impoverished compared with PG 3.X. ** Isabelle/Isar changes *** Support undo back into completed proofs (linear_undo). *** Electric terminator works without inserting terminator + Hit ; to process the last command. Easier than C-RET. *** Line numbers reported during script management @@ -89,7 +98,7 @@ ** Coq changes -*** Only supports Coq 8.1, support for earlier versions dropped. +*** Only supports Coq 8.1+, support for earlier versions dropped. *** Holes mode can be turned on/off and has its own minor mode -- cgit v1.2.3