Added code to register fully processed file. Multiple file fix list updated

2 files changed, 26 insertions, 10 deletions

diff --git a/generic/proof.el b/generic/proof.el
index 0965c400..9bc69480 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -847,7 +847,7 @@ Only call this from a scripting buffer."
 	       (setq buffer-display-table disp)))))
 
 (defun proof-mark-buffer-atomic (buffer)
-  "Mark BUFFER as having processed in a single step.
+  "Mark BUFFER as having been processed in a single step.
 
 If buffer already contains a locked region, only the remainder of the
 buffer is closed off atomically." 
@@ -1540,14 +1540,29 @@ locked region or everything in it has been processed."
 	(set-buffer script-buffer)
 	;; We only allow switching of the Scripting buffer if the
 	;; locked region is either empty or full for all buffers.
+	;; Here we check the current Scripting buffer's status.
 	(if (or 
 	     (eq (proof-unprocessed-begin) (point-min))
 	     (progn
 	       ;; Skip empty space at end of buffer
 	       (goto-char (point-max))
 	       (skip-chars-backward " \t\n")
-	       (>= (proof-unprocessed-begin) (point))))
-
+	       (if (>= (proof-unprocessed-begin) (point))
+		   ;; We're switching from a buffer which has been
+		   ;; completely processed.  Make sure that it's
+		   ;; registered on the included files list, in
+		   ;; case it has been processed piecemeal.
+		   (and buffer-file-name
+			;; FIXME: Could alter
+			;; proof-register-new-processed-file to work
+			;; also for possibly non-new cases.
+			(not
+			 (member buffer-file-truename 
+				 proof-included-files-list))
+			(progn
+			  (proof-register-new-processed-file file)
+			  ;; Continue 
+			  t)))))
 	    ;; we are changing the scripting buffer
 	   (progn
 	     (setq proof-active-buffer-fake-minor-mode nil)
diff --git a/todo b/todo
index 08d5f6af..78ac4df1 100644
--- a/todo
+++ b/todo
@@ -14,15 +14,16 @@ X (Low)    probably not worth wasting time on
 * This is a list of things which need doing in the generic interface
 ====================================================================
 
-A* shouldn't a
-    file that has been completed be added to proof-included-files-list?
+A* Fixup multiple files -- needs debugging.
 
-A* Fixup multiple files (mark atomic makes some assumption about
-   non-comment commands in script buffers).  Improve test for
-   locked region being whole of buffer.  This is partly done,
-   may need improvements.  (1hr)
+   1. mark atomic makes some assumption about non-comment commands in
+      script buffers
+      (partly fixed)
+   2. Improve test for locked region being whole of buffer
+      (probably fixed)
+   3. Management of proof-script-buffer-list maybe wrong.
 
-A* Check Info doc configuration with Emacs 20.2
+   (3hrs)
 
 C byte-compilation: check that byte compilation (and compiled code!)
   works for both varieties of Emacs.  Add instructions to INSTALL on