Updated

4 files changed, 42 insertions, 25 deletions

diff --git a/AUTHORS b/AUTHORS
index 3816baf0..68eb74ec 100644
--- a/AUTHORS
+++ b/AUTHORS
@@ -1,18 +1,19 @@
 Current Authors/Maintainers:
 
- David Aspinall <da@dcs.ed.ac.uk>	
-   doc, etc, generic, html, images, isa
- Patrick Loiseleur <Patrick.Loiseleur@lri.fr>    
-   coq
- Markus Wenzel <wenzelm@informatik.tu-muenchen.de>
-   isar
- Paul Callaghan <P.C.Callaghan@durham.ac.uk>
-   plastic, lego
+   David Aspinall <da@dcs.ed.ac.uk>	
+     doc, etc, generic, html, images, isa
+   Markus Wenzel <wenzelm@informatik.tu-muenchen.de>
+     isar
+   Paul Callaghan <P.C.Callaghan@durham.ac.uk>
+     plastic, lego
 
+>> Position vacant for Coq maintainer, offers welcome!
+ 
 Previous Authors:
 
-  Thomas Kleymann   (lego, doc, generic)
-  Healfdene Goguen  (coq, generic, doc)
-  Dilip Sequeira    (lego)
+   Thomas Kleymann   (lego, doc, generic)
+   Healfdene Goguen  (coq, generic, doc)
+   Dilip Sequeira    (lego)
+   Patrick Loiseleur (coq)
 
 
diff --git a/BUGS b/BUGS
index c5eb665a..6d53af9d 100644
--- a/BUGS
+++ b/BUGS
@@ -12,9 +12,10 @@ Generic problems
 ================
 
 * Highlighting of locked (blue) and queue (red) regions in FSF Emacs
-may be unreliable in some cases.  Cause unknown.  If you observe
-this, please submit a bug report with details of your system.  
-Workaround: switch to using XEmacs.
+may be unreliable (disappear) in some cases.  Cause unknown.  If you
+observe this, please submit a bug report with details of your system
+and any other information you think may be relevant.  Workaround:
+switch to using XEmacs.
 
 * Ordinary undo in script buffer can edit the "uneditable region"
 in XEmacs.  This doesn't happen in FSFmacs.  Test case:
diff --git a/COPYING b/COPYING
index 313f9451..4c53259b 100644
--- a/COPYING
+++ b/COPYING
@@ -12,15 +12,14 @@ Edinburgh.
 purposes.
 
 3. You accept Proof General "as is".  The University of Edinburgh
-makes no warranty in respect of Proof General.  Nevertheless you are
-encouraged to report to LFCS any problems with or suggestions for
-improvement of Proof General.
+provides no warranty of any kind in respect of Proof General.
+Nevertheless you are encouraged to report to LFCS any problems with or
+suggestions for improvement of Proof General.
 
 5. You may freely modify Proof General on condition that any
 significant changes are notified to LFCS and made available to LFCS
 such that they may be incorporated within future releases of 
-Proof General and licenced under the conditions of this licence
-agreement.
+Proof General under these copying conditions.
 
 6. You will acknowledge LFCS and The University of Edinburgh as the
 designers and implementors of Proof General in any relevant document
diff --git a/TODO b/TODO
index 21bc59c9..3efba2d0 100644
--- a/TODO
+++ b/TODO
@@ -3,15 +3,23 @@ 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!
 
-SHORT TERM
-----------
+Plan of Changes for Proof General 2.2
+--------------------------------------
+
 * Fix bugs and improve code and documentation
   Based on user feedback.  
 
-MEDIUM TERM
------------
-* Add an example instantiation of Proof General
-  using no prover-specific extensions (perhaps for Isabelle)
+* 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 
@@ -19,8 +27,16 @@ MEDIUM TERM
   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.