diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2004-02-08 15:26:25 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2004-02-08 15:26:25 +0000 |
| commit | 1355b2f4dcaf551aa6d804e74a440a73039b3606 (patch) | |
| tree | 530ea1771d175e42c49e3900ca0df17109adea57 /todo | |
| parent | 95c23599f31419bef3ae16c51611848df94f3763 (diff) | |
Updated.
Diffstat (limited to 'todo')
| -rw-r--r-- | todo | 11 |
1 files changed, 8 insertions, 3 deletions
@@ -3,20 +3,22 @@ $Id$ This is an outline file. Use C-c C-n, C-c C-p or menu to navigate. +================================================================= -* Proof General Short List of Things to Do for next version +* THINGS TO DO BEFORE 3.5 RELEASE *** Emacs Bug Roundup --- xemacs support for nested comments --- xemacs undo in read-only regions *** Clean up X-symbol support - -- token configuration for latest version of X-Symbol (Gerwin Klein) + -- token configuration for latest version of X-Symbol (Gerwin Klein, done?) -- remove on/off setting for all buffers (too slow), use same mechanism as proof-mmm. [Done; in testing] + -- Check x-symbol support in provers other than Isabelle *** Finish/cleanup MMM support for Isar. Document (but who reads it?) - Add MMM for other provers where relevant + Add MMM for other provers where relevant *** Isabelle support: can we somehow add "legacy" support for old theory files and even allow scripting in ML files? Maybe @@ -27,6 +29,9 @@ This is an outline file. Use C-c C-n, C-c C-p or menu to navigate. -- theorem dependencies on spoils ordinary response buffer output (dependency info *after* response display loses) +*** Check multiple file support in Isabelle -- maybe has become buggy + + * Proof General Infeasibly Long Low-Level List of Things to Do |