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

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

$Id$

See also the Proof General projects page on the web, under the
development section of the home page.  Also, see the appendix "Plans
and Ideas" in the manual, and for low-level detail, the file "todo" in
the developer release.

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


Plans for upcoming versions
---------------------------

* Support more proof assistants

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

* More flexible goals buffer mode to allow menus of common proof
  commands, especially via PBP-style highlighting

* Implement ideas in the Proof General White Paper. 
  (See the Development section of the web page for a link).

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

* Improve process handling: 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.

* Make an XEmacs package

* Repair byte-compilation