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
da+pg-feedback@inf.ed.ac.uk.  Thanks!


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

* Implement support for PG Kit.  Support PGIP provers fully, with/without 
  mediator.   (See http://proofgeneral.inf.ed.ac.uk/kit).

* Use CEDET Emacs framework for development tools, to allow more
  powerful parsing of proof scripts and features arising from that.  
  (See http://cedet.sourceforge.net/).

* 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

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

* Support more proof assistants.  Add more example proofs.

* Make an XEmacs package