diff options
| author | David Aspinall | 2004-04-16 09:33:35 +0000 |
|---|---|---|
| committer | David Aspinall | 2004-04-16 09:33:35 +0000 |
| commit | 43f05158948e421d3971fd85f0ed35d26a626187 (patch) | |
| tree | 50a073fb5dffb6976e5c3cc771b9cf8ebe428bf4 | |
| parent | 2dbce5c88bbf12e21c71f6e47337200a7a2bf070 (diff) | |
Updated.
| -rw-r--r-- | etc/announce | 7 | ||||
| -rw-r--r-- | todo | 9 |
2 files changed, 9 insertions, 7 deletions
diff --git a/etc/announce b/etc/announce index 5a28a99b..c614932e 100644 --- a/etc/announce +++ b/etc/announce @@ -21,7 +21,7 @@ Proof General includes these features, amongst others: . Provision to easily run proof assistant on a remote host . Works on any platform Emacs does, in window system or plain console -Summary of changes since 3.4: +Summary of interesting changes since 3.4: . Speedbar and Index Menu. Speedbar provides a handy file/tag tree. . Improved display management. @@ -29,10 +29,11 @@ Summary of changes since 3.4: . Keyboard hints and other messages displayed in minibuffer . Auxiliary modes bundled: X-Symbol and MMM Mode . Improved menus, user options, script colouring and active highlighting -. Many changes for compatibility with latest Emacsen (esp. GNU) and provers -. Many other minor improvements and editing features . For Coq: a new "holes" system, for editing structured expressions +. For Isabelle: browsing/highlighting theorem dependencies . New instances of PG: Casl Consistency Checker, Shell Script +. Many other minor improvements and editing features +. Many changes for compatibility with latest Emacsen (esp. GNU) and provers For details of changes since 3.4, see http://proofgeneral.inf.ed.ac.uk/fileshow.php?file=ProofGeneral-3.5%2FCHANGES @@ -5,21 +5,20 @@ This is an outline file. Use C-c C-n, C-c C-p or menu to navigate. ================================================================= -* THINGS TO DO BEFORE 3.5 RELEASE +* THINGS TO DO BEFORE/DURING 3.5 RELEASE *** Spam-protect email addresses on web pages *** Fixup HTML on mailing list pages *** Update documentation. + --- MMM support + --- Theorem dependencies *** Emacs Bug Roundup --- xemacs support for nested comments?? --- xemacs undo in read-only regions -*** Finish/cleanup MMM support for Isar. Document. - Add MMM for other provers where relevant - *** Isabelle tweaks -- theorem dependencies on spoils ordinary response buffer output (dependency info *after* response display loses) @@ -64,6 +63,8 @@ X (Low) e.g. probably not worth spending time on ** 2. Things to do in the generic interface +*** C Add MMM for other provers where relevant/useful + *** C Further display management improvement (it's a nightmare) Glitches to resolve: -- suggestion to cache window height: could implement this |