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
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59

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.

* Improve process handling 1: disable interrupts and/or catch
  errors at crucial points in code so that C-g can safely be
  used during script processing.


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.  

* Improve process handling 2: because Emacs is single-threaded,
  no process output can be dealt with when we are running some
  command.  This means that it would be safe to extend the 
  red region, by putting more commands on the queue.  Also it would
  be safe to implement a clever undo command which worked on the
  red region: if there are commands waiting to be processed, we
  could remove them from the queue.  If there are no commands waiting,
  we have to wait until something becomes blue to undo it by sending
  a command to the process.