blob: 91e55be5d3ddf42b9a203fa6bc119a5a556310ee (
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
|
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.
|