Updated

1 files changed, 18 insertions, 33 deletions

diff --git a/TODO b/TODO
index dbbdd6a6..c9d5fd66 100644
--- a/TODO
+++ b/TODO
@@ -1,59 +1,44 @@
 This is our brief list of planned things to do to Proof General.
 
+See also the appenix "Plans and Ideas" in the manual.
+
 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)
+Plans for later 3.x versions
+----------------------------
 
 * 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 
+* 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
+
+* Fix known problems with 3.0 (see developers `todo')
+
 
 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.
+
+* 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.
 
-* 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.
+* More flexible goals buffer mode to allow menus of
+  common proof commands.