blob: 333ba11452d057c4357155c3947db9b3b11bea1f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
This is a list of things which need doing to the lego mode.
* Fixing up errors caused by pbp-generated commands.
* undo support for LEGO needs to consider Discharge; perhaps unrol to
the beginning of the module?
* 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
* It would be nice to have a version ported to emacs19 (or
20). Unfortunately, it's currently impossible to port the pbp code,
since emacs19 doesn't properly handle highlighting of nested
overlays. The bulk of the stuff dependent on which version of emacs
is running has been moved to proof-dependencies.el, but there are
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
making help refer to the info file.
|
