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

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 and documentation
  Based on user feedback.  

MEDIUM TERM
-----------
* Add an example instantiation of Proof General
  using no prover-specific extensions (perhaps for Isabelle)

* 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.  Handle deleted buffers smoothly.


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.