Updated

3 files changed, 65 insertions, 46 deletions

diff --git a/AUTHORS b/AUTHORS
index 68eb74ec..0be05ffe 100644
--- a/AUTHORS
+++ b/AUTHORS
@@ -6,8 +6,8 @@ Current Authors/Maintainers:
      isar
    Paul Callaghan <P.C.Callaghan@durham.ac.uk>
      plastic, lego
-
->> Position vacant for Coq maintainer, offers welcome!
+   Pierre Courtieu <courtieu@lri.fr>
+     coq
  
 Previous Authors:
 
diff --git a/BUGS b/BUGS
index 2e002cd9..c82794c4 100644
--- a/BUGS
+++ b/BUGS
@@ -18,9 +18,9 @@ and any other information you think may be relevant.  Workaround:
 switch to using XEmacs.
 
 * Toolbar enablers for XEmacs 21: since these have been switched on,
-it is apparent that the recognition of completed proofs is unreliable.
-Please report cases where the buttons are enabled/disabled at the 
-wrong time.  
+it is apparent that the recognition of completed proofs may be
+unreliable (it wasn't used before).  Please report cases where the
+buttons are enabled/disabled at the wrong time.
 
 * Ordinary undo in the script buffer can edit the "uneditable region"
 in XEmacs.  This doesn't happen in FSFmacs.  Test case:
@@ -39,7 +39,7 @@ the best of all possible worlds, switch to XEmacs.
 breaks some of the code in Proof General, which is turned off in
 case the suspicious looking function
 toggle-enable-multibyte-characters is present.  This could effect
-forthcoming versions of XEmacs.
+forthcoming versions of XEmacs (but hasn't as far as XEmacs 21.1).
 Workaround: use FSFmacs 20.2, or XEmacs 20.4/later.
 
 * Using C-g can leave script management in a mess.  The code
@@ -47,9 +47,11 @@ needs to have some regions protected from Emacs interrupts.
 Workaround: Don't type C-g while script management is processing.  If
 you do, use proof-restart-scripting.
 
-* Outline-mode does not work in proof script files due to read-only
-restrictions of protected region.  Workaround: none, nevermind.
-(If it's hugely needed we could support modified outline commands).
+* Outline-mode does not work in processed proof script files due to
+read-only restrictions of the protected region.  This is an inherent
+problem with outline because it works by modifying the buffer.
+Workaround: none, nevermind.  (If it's hugely needed we could support
+modified outline commands).
 
 * `proof-find-next-terminator' (bound to C-c C-e) doesn't work
 properly.  Neither does 'proof-goto-command-start' (C-c C-a).
@@ -70,42 +72,22 @@ recommended way of working) is to run XEmacs locally and only
 the proof assistant on your fast compute server, by setting 
 proof-rsh-command.
 
-* There is an problem with process communication on Solaris, where
-there is an input line length limitation for terminals in cooked mode,
-perhaps to 256 characters.  Further input elicits a bell character
-(^G).  This ruins Proof General's parsing of the shell buffer.
-Future fix: try setting process-connection-type to nil, which
-instructs XEmacs to use pipes instead of pseudo-terminals for
-subprocess I/O.  (You lose job control of processes you start in shell
-mode, and some commands (notably ls) behave differently when writing
-output to a pipe instead of a tty.  But using a pipe will allow you to
-paste arbitrarily long blocks of text into shell mode.)
-Current workaround:  use another OS, e.g. Linux.
-[1999/08/20: believed to be fixed]
-
-* XEmacs sessions maybe 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.  
-[1998/10/06: believed to be fixed]
-
 * When proof-rsh-command is set to "ssh host" and you issue Ctrl-c to
 interrupt, the whole process may be killed instead of interrupted.
 This isn't a bug in Proof General, but the behaviour of ssh.  Try
 using rsh instead, it is said to forward signals to the remote command.
 
-FSF Emacs specific bugs
-=======================
 
-*`proof-zap-commas-region' does not work for Emacs 20.2 on
-  lego/example.l . On *initially* fontifying the buffer,
-  commas are not zapped. However, when entering text, commata are
-  zapped correctly. Workaround: don't stare too much at commata
 
 
 LEGO Proof General Bugs
 =======================
 
+* [FSF specific] `proof-zap-commas-region' does not work for Emacs
+  20.2 on lego/example.l . On *initially* fontifying the buffer,
+  commas are not zapped [unfontified]. However, when entering text,
+  commata are zapped correctly. Workaround: don't stare too much at commata
+
 * If LEGO attempts to write a (object) file in a non-writable
   directory, it forgets the protocol mechanism on how to interact with 
   Proof General and gets stuck. Workaround: Directly enter "Configure
@@ -161,15 +143,16 @@ as you might expect.  This probably has no detrimental impact on the
 interface unless you use your own "goal" or "qed" forms.
 
 * Blocking when processing multiple files, beginning from a .ML file.
-Proof General will block the Emacs process when it is waiting for
-a theory file (and it's ancestors) to be read.  To avoid this,
-assert the theory file rather than the ML file, or use C-c C-s
-to start scripting before using one of the assertion commands.
+Proof General will block the Emacs process when it is waiting for a
+theory file (and it's ancestors) to be read.  To avoid this, assert
+the theory file rather than the ML file, or use C-c C-s to start
+scripting (which triggers reading the theory) before using one of
+the assertion commands.
 
 * Cut-and-paste from Isabelle output (e.g. goals buffer) is
 problematic.  You will find that this inserts otherwise-invisible
 special characters into the script buffer, which are used to do the
 highlighting.  If you really need to do cut-and-paste, customize the
 variable proof-shell-leave-annotations-in-output to nil.
-Unfortunately this will turn off highlighting.
+Unfortunately this will turn off variable colouring.
 
diff --git a/todo b/todo
index bfcee187..69673a8d 100644
--- a/todo
+++ b/todo
@@ -51,15 +51,39 @@ re-enabled), proof-toggle-scripting, new configuration options.
     - Fix sentinel infinite loop bug
     - noticeable delay when loading ML files for Isabelle (fontification?)
 
-A Isabelle (and perhaps other prover) multiple file problem: 
-  add configuration setting proof-shell-inform-file-processed-command,
-  and send *retract* action when reactivating scripting in a previously
-  full buffer, but don't actually unlock there.  
-
-A Nested error problem:  conceptually, activate scripting should fail
+B Fixing up PBP: things almost work for lego (apart from getting
+   pbp wrong!) -- there is a bug with (newline-and-indent) though
+   which tries to write into the locked region for some reason.
+
+C IDEAS FOR SIMPLIFIED PROVER INSTANTIATION.
+  We could make extensive use of defvaralias to automatically
+  declare the settings for each proof assistant.  Then the 
+  tedious "shadowing" (or copying) is done automatically.  
+  e.g. 
+
+C Improved configurability of command settings, etc.
+  We should let command settings, etc, be a special type
+  which can be one of three things:
+
+    'string    -- send this as a command to assistant
+    'function  -- call this interactively to return either
+		   'string -- send this as a command
+		    nil -- do nothing (function does work).
+				   
+  This way we cover commands which need prompting for extra
+  args, as well as elisp functions which do whatever's necessary.
+  Then use a generic function "proof-invoke-function" or similar.
+
+C C-x C-v does not seem to run kill buffer hooks properly: at
+  least, what happens is buffer name changes to **lose** and
+  (e.g.) a completely processed file doesn't get added to the
+  included files list.  Auto retraction appears to work.
+
+B Nested error problem:  conceptually, activate scripting should fail
   if the hook function which causes loading of more files (for isabelle)
   fails.  Maybe fix by adding a new piece of state: 
-  "proof-shell-error-flagged".
+  "proof-shell-error-flagged" and testing it before allowing
+  scripting to start.
 
 B Add something to better document two-buffer versus three-buffer
   interaction modes, and the use of proof-window-dedicated to
@@ -729,6 +753,18 @@ D Improve coqtags. It cannot handle lists e.g., with
 * Things to do for Isabelle
 ===========================
 
+B Stuff with x-symbols mentioned by DvO:
+
+    I've noticed a problem at least with xemacs 20.3: After
+    Goal "A\\<longrightarrow>a";
+    qed "x";
+    in the error message (unsolved goals), the x-symbol is not printed
+    correctly. This has to do with 
+	  (proof-x-symbol-decode-region start (point))
+    in proof-response-buffer-display. For some reason, this problem does
+    not arise when a tactic fails, e.g.
+    by (subgoal_tac "+nonsense" 1);
+
 B auto-adjust Pretty.setmargin when window is resized
 
 C Unify display of proof output for final level "No subgoals"