From 61e83559cb7614a71834f3c513c6638d54e89904 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 27 Jun 2000 15:27:44 +0000
Subject: Updated

---
 TODO | 18 +++++++++++-------
 todo |  5 -----
 2 files changed, 11 insertions(+), 12 deletions(-)

diff --git a/TODO b/TODO
index 4fc5eb3e..4051676f 100644
--- a/TODO
+++ b/TODO
@@ -17,22 +17,26 @@ Plans for upcoming 3.x versions
 
 * Support turning on/off prover output automatically, e.g.
   Coq's "Begin Silent" and "End Silent" commands.
+  [Now implemented in 3.2pre]
 
 * Fix Isabelle's "Stack overflow in regexp".   See isa/BUGS.
-
-* Make an XEmacs package
-
-* Support more proof assistants
+  [Now implemented in 3.2pre]
 
 * New key bindings for prover specific commands.  
   This will unfortunately result in changing some bindings, but make
   room for more and avoid the user-reserved sequences C-c <letter>.
-
-* A more flexible way of choosing which instance of PG we want,
-  allowing matches on the buffer before choosing the mode function.
+  [Now implemented in 3.2pre]
 
 * Add a favourites mechanism for proof commands issued using
   point-and-click in goals buffer.  Useful when pbp isn't supported.
+  [Now partially implemented in 3.2pre]
+
+* Make an XEmacs package
+
+* Support more proof assistants
+
+* A more flexible way of choosing which instance of PG we want,
+  allowing matches on the buffer before choosing the mode function.
 
 * Isabelle PG: Non-blocking for .thy loading from .ML files.
 
diff --git a/todo b/todo
index 7a1dbba5..a4e10afc 100644
--- a/todo
+++ b/todo
@@ -29,11 +29,6 @@ X (Low)		e.g. probably not worth spending time on
 
 *** Outstanding bugs to investigate
 
-A Re-visiting files (in Isar, at least) doesn't lock them properly.
-  M-x isar-mode does.  Why?
-  Also, when files are removed by typing in shell buffer, they
-  don't get uncoloured???
-
 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.
-- 
cgit v1.2.3