diff options
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 20 |
1 files changed, 14 insertions, 6 deletions
@@ -8,6 +8,18 @@ ** Generic Changes +*** New more efficient and generalised parsing functions + + Also works around crash bug in xemacs-21.1.7/SuSE. + Fix to previous function (used by FSF Emacs) by Markus Wenzel. + XEmacs uses new functions which have slightly different + behaviour. If this is problematical, please report, and + force the use of the old function by writing: + + (defalias 'proof-segment-up-to 'proof-segment-up-to-old) + + in your .emacs file. (Warning: only during pre-release!) + *** Makefile has new target "scripts" to fix paths in bash/perl scripts *** Bug fix: "next" button enabled more often. Solaris turns off enablers. @@ -18,7 +30,8 @@ for provers need initialization before synchronization can be secured. [Developers note: LEGO needs to wait for second prompt before sync, whereas Isabelle managed to sync on first prompt. Coq was best, - with sync set before startup, using a command line option.] + with sync set before startup, using a command line option. + That is the recommended route for new proof assistants.] *** Bug fix: script management is now more robust against C-x C-v, C-x C-w @@ -46,11 +59,6 @@ It's nicer to do this manually if you like this mode, using M-x proof-goto-end-of-locked. -*** Efficiency improvement in parsing - - Also works around crash bug in xemacs-21.1.7/SuSE. - Fix by Markus Wenzel. - *** Added possibility for switching prover's output on/off. Already implemented in Coq and Isabelle(/Isar). |