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 2.2 -------------------------------------- * Fix bugs and improve code and documentation Based on user feedback. * Queue manipulation improvment: allow to extend or reduce during processing, with fewer "Proof Process Busy" messages. * Font-lock based on annotations in proof assistant output. Particularly: colouration for Isabelle variable names. * x-symbol support integration. * 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. MEDIUM TERM ----------- * Add an example instantiation of Proof General using no prover-specific extensions (perhaps for Isabelle) 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.