diff options
| author | Dilip Sequiera | 1997-11-26 17:49:06 +0000 |
|---|---|---|
| committer | Dilip Sequiera | 1997-11-26 17:49:06 +0000 |
| commit | 804c446ae609a4acfec4c5eabbd84ef55a262e11 (patch) | |
| tree | 45915f8f9d060a0fbdd58545ba2c64a9f507345d /todo | |
| parent | aa910d291903d518325f3a74aaaffe13a1a38e29 (diff) | |
Noted bug in popup-eager-annotation
Diffstat (limited to 'todo')
| -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. |