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

See also the appenix "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 later 3.x versions
----------------------------

* Addition of favourites mechanism for proof commands issued using
  point-and-click in goals buffer.  Useful when pbp isn't supported.

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

* 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


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

* Implement "Atomic Command Sequence" idea, or something like
  it.  To allow more flexible understanding of undo behaviour
  of proof assistants.  Alternative is to base markup of 
  undoable regions on proof assistant output or messages.

* Add completion of theorem names, choice of proof commands, etc.

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

* More flexible goals buffer mode to allow menus of
  common proof commands.