Added proof-shell-inform-file-processed-command setting.

2 files changed, 63 insertions, 25 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index e8757747..7778ba11 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -116,13 +116,26 @@ If 'ignore, point is never moved after toolbar movement commands."
 
 (defcustom proof-window-dedicated nil
   "*Whether response and goals buffers have dedicated windows.
-If t, windows displaying responses from the prover will not
-be switchable to display other windows.  This may help manage
-your display, but can sometimes be inconvenient, especially
-for experienced Emacs users.
-Moreover, this option may cause problems with multi-frame
-use because of a bug."
-  :type 'boolean
+If non-nil, Emacs windows displaying messages from the prover will not
+be switchable to display other windows.
+
+This option can help manage your display.
+
+Setting this option triggers a three-buffer mode of interaction where
+the goals buffer and response buffer are both displayed, rather than
+the two-buffer mode where they are switched between.  It also prevents
+Emacs automatically resizing windows between proof steps.  
+
+If you use several frames (X windows), you can force a frame to stick
+to showing the goals or response buffer.
+
+For single frame use this option may be inconvenient for
+experienced Emacs users."  
+  ;; Did say: 
+  ;; Moreover, this option may cause problems with multi-frame 
+  ;; use because of a bug.  
+  ;; but I can't find it as of 3.0pre201099.  
+  :type 'boolean 
   :group 'proof-general)
 
 (defcustom proof-strict-read-only 
@@ -912,6 +925,25 @@ script everytime scripting begins."
   :type 'string
   :group 'proof-shell)
 
+(defcustom  proof-shell-inform-file-processed-command nil
+ "Command to the proof assistant to tell it that a file has been processed.
+The format character %s is replaced by a complete filename for a
+script file which has been fully processed interactively with
+Proof General.  
+
+This is used to interface with the proof assistant's internal
+management of multiple files, so the proof assistant is kept aware of
+which files have been processed.  Specifically, when scripting
+is deactivated in a completed buffer, it is added to Proof General's
+list of processed files, and the prover is told about it by
+issuing this command.
+
+If this is set to nil, no command is issued.
+
+See also proof-shell-process-file, proof-shell-compute-new-files-list."
+ :type '(choice string (const nil))
+ :group 'proof-shell)
+
 
 ;;
 ;; 5b. Regexp variables for matching output from proof process.
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 4bbb7d25..0c801cf9 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -429,26 +429,30 @@ to allow other files loaded by proof assistants to be marked read-only."
 		    :test 'equal)))
     (and pos (nth pos buffers))))
 
-(defun proof-register-possibly-new-processed-file (file)
-  "Register a possibly new FILE as having been processed by the prover."
+(defun proof-register-possibly-new-processed-file (file &optional informprover)
+  "Register a possibly new FILE as having been processed by the prover.
+If INFORMPROVER is non-nil, the proof assistant will be told about this,
+to co-ordinate with its internal file-management."
   (let* ((cfile (file-truename file))
 	 (buffer (proof-file-to-buffer cfile)))
     (proof-debug (concat "Registering file " cfile 
 			 (if (member cfile proof-included-files-list)
-			     " (already registered)." ".")))
-    (if (not (member cfile proof-included-files-list))
-	(progn
-	  (and buffer
-	       (buffer-modified-p buffer)
-	       (proof-warning (concat "Changes to "
-				      (buffer-name buffer)
-				      " have not been saved!")))
-	  (setq proof-included-files-list
-		(cons cfile proof-included-files-list))
-	  ;; If the file is loaded into a buffer, put an
-	  ;; atomic locked region in it.
-	  (if buffer
-	      (proof-complete-buffer-atomic buffer))))))
+			     " (already registered, no action)." ".")))
+    (unless (member cfile proof-included-files-list)
+      (and buffer
+	   (buffer-modified-p buffer)
+	   (proof-warning (concat "Changes to "
+				  (buffer-name buffer)
+				  " have not been saved!")))
+      (setq proof-included-files-list
+	    (cons cfile proof-included-files-list))
+      ;; If the file is loaded into a buffer, make sure it is completely locked
+      (if buffer
+	  (proof-complete-buffer-atomic buffer))
+      ;; Tell the proof assistant, if we should and if we can
+      (if (and informprover proof-shell-inform-file-processed-command)
+	  (proof-shell-invisible-command 
+	   (format proof-shell-inform-file-processed-command cfile))))))
 
 (defun proof-unregister-buffer-file-name ()
   "Remove current buffer's filename from the list of included files.
@@ -583,10 +587,12 @@ a scripting buffer is killed it is always retracted."
 
 	      (if (proof-locked-region-full-p)
 		  ;; If locked region is full, make sure that this buffer
-		  ;; is registered on the included files list.
+		  ;; is registered on the included files list, and
+		  ;; let the prover know it can consider it processed.
 		  (if buffer-file-name
 		      (proof-register-possibly-new-processed-file 
-		       buffer-file-name)))
+		       buffer-file-name
+		       'tell-the-prover)))
 	      
 	      (if (proof-locked-region-empty-p)
 		  ;; If locked region is empty, make sure this buffer is