diff options
| -rw-r--r-- | todo | 8 |
1 files changed, 5 insertions, 3 deletions
@@ -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. |