Updated

1 files changed, 11 insertions, 7 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.