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
60
61
62
63
64

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!

Plan of Changes for Proof General 3.0
-------------------------------------

* Fix bugs and improve code and documentation
  Based on user feedback.  

* Font-lock based on annotations in proof assistant output.
  Particularly: colouration for Isabelle variable names.

* x-symbol support integration.

* More toolbar buttons.  Improvement of menus.


Plans for later versions
------------------------

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

* Queue manipulation improvment: allow to extend or reduce
  during processing, with fewer "Proof Process Busy"
  messages.  

* Isabelle PG: Non-blocking for .thy loading from .ML files.
  (hopefully as happy side effect of queue improvement)

* 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.


Plans for even later versions
-----------------------------

* 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.