From 3d2978cf896be29b579cb56b6c33b867d093b587 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 5 May 2000 15:09:21 +0000 Subject: Updated --- CHANGES | 12 ++++++++++++ todo | 7 +++++++ 2 files changed, 19 insertions(+) diff --git a/CHANGES b/CHANGES index 984f7ab4..a5bb26d5 100644 --- a/CHANGES +++ b/CHANGES @@ -15,6 +15,12 @@ *** Improved behaviour of electric terminator +*** Point never moves if proof-follow-mode is 'ignore. + + Previously it was always moved when an error occurred. + 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. @@ -37,10 +43,16 @@ ** Isabelle Changes +*** More code from Isamode has been merged into Proof General + + Particularly: the user now can choose a logic image from inside PG. + *** Fix for stack overflow in regexp which occurred with large proof states ** Isar Changes +*** Fix for stack overflow in regexp which occurred with large proof states + ** HOL Changes *** Output decoration improvements. diff --git a/todo b/todo index 50f8b32f..ce7db622 100644 --- a/todo +++ b/todo @@ -29,6 +29,8 @@ X (Low) e.g. probably not worth spending time on *** Outstanding bugs to investigate +A find C-c C-l binding and remove it. Overriden with goto-end-of-locked. + C Undoing comments with FSF Emacs weirdness. Noticed with Emacs 20.6.1. Seems to affect all provers. Workaround: use C-c C-RET or C-c C-r instead. @@ -44,6 +46,11 @@ C Problem with startup for Coq and HOL. See BUGS. *** Scheduled improvements for 3.2 **** A Doc new bits: font lock keywords, filename %e, %r. + Added proof-{script,shell,goals,resp}-font-lock-keywords. + Presently used only in proof-easy-config, will put into other + mechanism for 3.2 + +**** A Doc new bits: Isabelle settings mechanism, win32 support **** A Add a new keymap(s) for proof assistants. Presently they naughtily bind C-c which are reserved for -- cgit v1.2.3