TODO


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

This is our brief list of planned things to do to Proof General.

Please send any suggestions, comments, or offers of help to
proofgen@dcs.ed.ac.uk.  Thanks!

SHORT TERM
----------
* Fix bugs and improve code

MEDIUM TERM
-----------
* Revise and improve the documentation

* Provide a sensible default frame/buffer layout

* Add an example instantiation of Proof General
  with no prover-specific extensions
  (probably for Isabelle)

* Implement a new buffer model:

    1. Script buffers
    2. Response buffer
    3. (optionally part of response buffer) goals buffer
    4. (hidden) process buffer
    5. Minibuffer for additionally sending information to the process

* Add support for putting a locked region in processed files,
  and querying the process about which files have been processed.

LONGER TERM
-----------
* Add a browser mode for browsing script files and/or
  theory data-structures in the prover.

* Add more per-prover functions: menus for tactics, etc.