blob: f4af3662438faf59b30d98c630688a0a89912c88 (
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
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
|
-*- mode:outline -*-
* This is a list of things which need doing in the generic interface
====================================================================
o Implement proof-find-previous-terminator and bind it to C-c C-a
o Fixing up errors caused by pbp-generated commands.
o 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.
o 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.
o file handling could be more robust
o LEGO and Coq modes overwrite each other.
o We need to go over to piped communication rather than ptys to fix
the (Solaris) ^G bug. In this circumstance there's a bug in the
eager annotation code
* Here are things to be done to Lego mode
=========================================
o undo support for LEGO needs to consider Discharge; perhaps unrol to
the beginning of the module?
o LEGO mode might incorporate changes to Coq mode menu, in particular
making help refer to the info file.
* Here are things to be done to Coq mode
========================================
o Restart if going back to beginning of proof.
o C-c u inside a Section should reset the whole section, then redo defns
o There's a bug so the goal buffer isn't displaying everything that
happens.
o Sections and files are handled incorrectly.
o Update documentation to include C-c C-s.
o Lifted nested lemmas respond incorrectly to C-c u: Coq gets sent the
correct command if I undo up to the lower lemma, but the buffer
undoes to the upper lemma. I.e., if I start Lemma x, then prove
Lemma y, then finish x, and undo lemma x, then lemma y gets undone
in the buffer as well.
|
