Noted bug in popup-eager-annotation

1 files changed, 5 insertions, 3 deletions

diff --git a/todo b/todo
index 35982946..56c5eacc 100644
--- a/todo
+++ b/todo
@@ -8,6 +8,7 @@ This is a list of things which need doing to the lego mode.
 * pbp code doesn't quite accord with the tech report; in particular it
   decodes annotations eagerly. Lazily would be faster, and it's what
   the tech report claims
+  --- djs: probably not much faster, actually.
 
 * It would be nice to have a version ported to emacs19 (or
   20). Unfortunately, it's currently impossible to port the pbp code,
@@ -17,9 +18,6 @@ This is a list of things which need doing to the lego mode.
   doubtless differences in font-locking and menu code which will
   require some work.
 
-* Indentation - LEGO should indent only with brackets; Coq for Inductive
-  definitions and 'case' constructs also. LEGO NOW DONE.
-
 * file handling could be more robust
 
 * LEGO mode might incorporate changes to Coq mode menu, in particular
@@ -27,6 +25,10 @@ This is a list of things which need doing to the lego mode.
 
 * LEGO and Coq modes overwrite each other.
 
+* We need to go over to piped communication rather than ptys to fix the
+  ^G bug. In this circumstance there's a bug in the eager annotation
+  code
+
 Here are things to be done to Coq mode:
 
 * Restart if going back to beginning of proof.