Updated

2 files changed, 41 insertions, 45 deletions

diff --git a/BUGS b/BUGS
index 373beabd..2c6ab283 100644
--- a/BUGS
+++ b/BUGS
@@ -1,20 +1,30 @@
-
 Known bugs and workarounds.
 ===========================
 
+* Outline-mode does not work in proof script files due to read-only
+restrictions of protected region
+
+* You can't use more than one proof assistant at a time in the same
+Emacs session.  Workaround: use more than one Emacs session, with
+different settings of the variable proof-assistant.
 
+* There is an obscure bug with processes on Solaris which results in
+buffers full of ^G after certain combinations of input.  Workaround:
+get a patch from Sun, or use Linux.
 
 
 
+Development  (move these above once decided not to fix):
+========================================================
+
+XEmacs sessions seem to grow excessively in terms of memory
+allocation. Maybe some of the spans aren't removed properly.
+Setting a limit on the size of the process buffer doesn't seem to
+help. 
 
-Development:
-============
 
 customize:  odd behaviour after setting proof-assistant in
 .emacs file via customize: customize reports "mismatch"
 and "set outside customize".  Second of these probably
 okay.  Why first?
 
-
-da: How to remove a directory from CVS?  I think it needs
-editing in the repository.  'isabelle' is defunct.
diff --git a/todo b/todo
index 81ee9422..177099d1 100644
--- a/todo
+++ b/todo
@@ -12,7 +12,7 @@ X (Low)    probably not worth wasting time on
 * This is a list of things which need doing in the generic interface
 ====================================================================
 
-B proof-toolbar:  Add support for entering a goal and saving a theorem
+A proof-toolbar:  Add support for entering a goal and saving a theorem
   at the generic level.  These functions should also
   be accessible from menus.  Fixup movement of point (choice of
   up and down functions).  Add toolbar to pbp mode too.  
@@ -26,11 +26,6 @@ X Improve toolbar icons.  Automatically generate reduced and
   xcf files under CVS rather than xpm files.
   (5h or more to design nice ones)
 
-A Remove defunct "isabelle" directory.  All collbarators must
-  synchronize and remove their working directories to do this,
-  because we need to operate on the repository directly.
-  (da, 5min).
-
 A Documentation for proof-mode and its derived modes.  (5min)
 
 A Clean up proof-assert-until-point behaviour.  At the moment we
@@ -46,7 +41,7 @@ A Clean up proof-assert-until-point behaviour.  At the moment we
   proof-assert-next-command does not advance point. 
   (da, tms/others to assess)
   
-B A less drastic version of proof-restart-script would be useful:
+A A less drastic version of proof-restart-script would be useful:
   one that doesn't involve killing off the proof assistant process
   and restarting that -- it can take ages!  (da, 20mins)
 
@@ -57,8 +52,7 @@ D Code in proof.el assumes all characters with top bit set are special
 A Add a small script "example.l" etc to each of the prover subdirectories,
   for testing/example purposes.  (Perhaps proving the same thing?
   commutativity of conjunction?) 
-  Only needed for Coq now.
-  (10min, tms)
+  Only needed for Coq now.   (10min, hhg)
 
 D Prune dead code.  (1h)
 
@@ -83,11 +77,14 @@ B Fixup sources to follow Elisp conventions better.
   The first line of documentation of functions and
   variables should be a whole sentence.  Subsequent lines should
   *not* be indented.  See output of hyper-apropos and
-  poor formatting of current comments.   (1hr)
+  poor formatting of current comments.   (1hr, tms)
 
 A Update source documentation and manual, in particular document bugs
   and workarounds
-  (4h hhg & tms) 
+  (4h hhg & tms & da) 
+
+D Technical documentation to record expertise and allow users of other
+  proof systems to adopt generic package (40h hhg & tms)
 
 A Implement more generic mechanism for large undos (2h)
 
@@ -107,15 +104,10 @@ A Multiple files are sometimes handled incorrectly, because the
 D Implement proof-find-previous-terminator and bind it to C-c C-a
   (45min tms)
 
-D Technical documentation to record expertise and allow users of other
-  proof systems to adopt generic package (40h hhg & tms)
-
-D Support for x-symbols package 
-
-X XEmacs sessions seem to grow excessively in terms of memory
-  allocation. Perhaps some of the spans aren't removed properly?
-  Setting a limit on the size of the process buffer doesn't seem to
-  help. 
+D Support for x-symbols package.
+  Provers with sophisticated/configurable syntax should tell Emacs
+  about their syntax somehow, rather than trying to duplicate
+  specifications inside Emacs.
 
 A file handling could be more robust; perhaps one should always cd to
   the directory corresponding to the script buffer (currently only
@@ -127,14 +119,14 @@ A replace (current-buffer) by proof-shell-buffer/proof-script-buffer
   where ever possible (30 min tms)
 
 A Replace "You are not authorised for this information." by a proper
-  documentation (2h)
+  documentation (2h, da)
 
 A Reengineer *-count-undos and *-find-and-forget at generic level
-    (3h)
+  (3h)
 
 D Allow bib-cite style clicking on Load/Import commands to go to file.
 
-X LEGO and Coq modes overwrite each other.
+D support font-lock in goal buffer
 
 X We need to go over to piped communication rather than ptys to fix
   the (Solaris) ^G bug. In this circumstance there's a bug in the
@@ -142,13 +134,11 @@ X We need to go over to piped communication rather than ptys to fix
   tested for future versions. [Currently the problem is documented in
   Email messages sent to lego]
 
-X Outline-mode does not work due to read-only restrictions of
-  protected region
-
-D support font-lock in goal buffer
-
 B Introduce keybinding to save the proof e.g., in LEGO, this should
   insert "Save id" or "$Save id" depending on the name of the theorem. 
+  Do the same thing for Goal, to add as a toolbar function.
+
+B Unify toolbar and menu functions.
 
 D use proof buffer instead of response buffer and leave non-proof
   state output in the process buffer (1h)
@@ -156,12 +146,6 @@ D use proof buffer instead of response buffer and leave non-proof
 D Remove duplication of variables e.g., proof-prog-name and
   lego-prog-name for Coq and Lego. (1h)
 
-D As well as duplicated variables, we also have duplicated modes,
-  which could be removed.  We never use proof-shell-mode, proof-mode,
-  pbp-mode, only the derived instances.
-  Shouldn't the generic interface directly *define* the derived
-  version required?   (1h to fix)
-
 D Fixup implementation of "spans":  Add documentation!
   (30 mins)
 
@@ -177,17 +161,19 @@ X Comment support is not very generic: we don't support end-of-line
 A Fixing up errors caused by pbp-generated commands; currently, script
   management unwisely assumes that pbp commands cannot fail (2h tms)
 
-A Rename pbp-mode to response-mode (which doesn't support any actual
-  proof-by-pointing) (30min) 
+A Rename pbp-mode to response-mode or goals-mode (which doesn't
+  support any actual proof-by-pointing) (30min) 
 
-A Outsource actual pbp functionality (30min)
-    (separate pbp annotations from other annotations)
+A Outsource actual pbp/goals functionality (30min)
+  (separate pbp annotations from other annotations).
+  Make a file proof-goals.el.
 
 X pbp code doesn't quite accord with the tech report; in particular it
   decodes annotations eagerly. Lazily would be faster, and it's what
   the tech report claims
   --- djs: probably not much faster, actually.
 
+
 * Here are things to be done to Lego mode
 =========================================
 
@@ -275,7 +261,7 @@ D The proof-locked-span isn't set to read-only, because overlays don't
 * Release
 =========
 
-A remove CVS history in all files  (replace with idents $Id$)
+A remove CVS history in all files  (replace with idents $Id)
 
 A extend Copyright to 1998