Added symmetric proof-shell-inform-file-retracted-cmd setting to correspond

with the state change of a buffer from completely processed to
partly processed.

2 files changed, 103 insertions, 28 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index a2c34b59..aebda133 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -591,13 +591,16 @@ You must set this variable."
 
 (defcustom proof-comment-start ""
   "String which starts a comment in the proof assistant command language.
-The script buffer's comment-start is set to this string plus a space."
+The script buffer's comment-start is set to this string plus a space.
+Moreover, comments are ignored during script management, and not
+sent to the proof process."
   :type 'string
   :group 'proof-script)
 
 (defcustom proof-comment-end ""
   "String which ends a comment in the proof assistant command language.
-The script buffer's comment-end is set to this string plus a space."
+The script buffer's comment-end is set to this string plus a space.
+See also `proof-comment-start'."
   :type 'string
   :group 'proof-script)
 
@@ -739,16 +742,19 @@ attempted, so the setting of this variable doesn't matter."
   :group 'proof-script)
 
 (defcustom proof-lift-global nil
-  "This function lifts local lemmas from inside goals out to top level.
-This function takes the local goalsave span as an argument. Set this
-to `nil' if the proof assistant does not support nested goals."
+  "Function which lifts local lemmas from inside goals out to top level.
+This function takes the local goalsave span as an argument. Leave this
+set this at `nil' if the proof assistant does not support nested goals,
+or if you don't want to write a function to do move them around."
   :type 'function
   ;; FIXME customize broken on choices with function in them?
   ;; :type '(choice (const :tag "No local lemmas" nil) (function))
   :group 'proof-script)
 
 (defcustom proof-count-undos-fn nil 
-  "Compute number of undos in a target segment"
+  "Function to compute number of undos in a target segment.
+This is an important function for script management.
+Study one of the existing instantiations for examples of how to write it."
   :type 'function
   :group 'proof-script)
 
@@ -783,7 +789,10 @@ Only relevant for proof-find-and-forget-fn.")
   "Function that returns a command to forget back to before its argument span.
 This setting is used to for retraction (undoing) in proof scripts.
 
-The special string proof-no-command means there is nothing to do."
+The special string proof-no-command means there is nothing to do.
+
+This is an important function for script management.
+Study one of the existing instantiations for examples of how to write it."
   :type 'function
   :group 'proof-script)
 
@@ -819,7 +828,9 @@ commands which should be entered directly into the script itself."
 The current buffer will be the newly active scripting buffer.
 
 This hook may be useful for synchronizing with the proof
-assistant, for example, to switch to a new theory."
+assistant, for example, to switch to a new theory
+(in case that isn't already done by commands in the proof
+script)."
   :type '(repeat function)
   :group 'proof-script)
 
@@ -877,7 +888,7 @@ parentheses and commands. It represents these with the characters
 ;;
 
 (defcustom proof-prog-name nil
-  "System command to run program name in proof shell.
+  "System command to run the proof assistant in the proof shell.
 Suggestion: this can be set in proof-pre-shell-start-hook from
 a variable which is in the proof assistant's customization
 group.  This allows different proof assistants to coexist
@@ -893,7 +904,7 @@ print a welcome message.
 Note that it is sent before Proof General's synchronization
 mechanism is engaged (in case the command engages it).  It
 is better to configure the proof assistant via command
-line options is possible."
+line options if possible."
    :type '(choice string (const nil))
    :group 'proof-shell)
 
@@ -921,7 +932,7 @@ directory the file resides in.
 
 NB: By default, proof-cd is called from proof-activate-scripting-hook,
 so that the prover switches to the directory of a proof
-script everytime scripting begins."
+script every time scripting begins."
   :type 'string
   :group 'proof-shell)
 
@@ -940,7 +951,30 @@ 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."
+See also: proof-shell-inform-file-retracted-cmd, 
+proof-shell-process-file, proof-shell-compute-new-files-list."
+ :type '(choice string (const nil))
+ :group 'proof-shell)
+
+(defcustom  proof-shell-inform-file-retracted-cmd nil
+ "Command to the proof assistant to tell it that a file has been retracted.
+The format character %s is replaced by a complete filename for a
+script file which Proof General wants the prover to consider
+as not completely processed.
+
+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 activated, the file is removed from Proof General's list of 
+processed files, and the prover is told about it by issuing this 
+command.  The action may cause the prover in turn to suggest to 
+Proof General that files depending on this one are
+also unlocked.
+
+If this is set to nil, no command is issued.
+
+See also: proof-shell-inform-file-processed-cmd, 
+proof-shell-process-file, proof-shell-compute-new-files-list."
  :type '(choice string (const nil))
  :group 'proof-shell)
 
@@ -950,7 +984,7 @@ See also proof-shell-process-file, proof-shell-compute-new-files-list."
 ;;
 
 (defcustom proof-shell-prompt-pattern nil 
-   "Proof shell's value for comint-prompt-pattern."
+   "Proof shell's value for comint-prompt-pattern, which see."
    :type 'regexp
    :group 'proof-shell)
 
@@ -1004,9 +1038,9 @@ It is safe to leave this variable unset (as nil)."
 
 (defcustom proof-shell-interrupt-regexp nil
   "Regexp matching output indicating the assistant was interrupted.
-We assume that an error message corresponds to a failure in the last
+We assume that an interrupt message corresponds to a failure in the last
 proof command executed.  So don't match mere warning messages with
-this regexp.  Moreover, an error message should not be matched as an
+this regexp.  Moreover, an interrupt message should not be matched as an
 eager annotation (see proof-shell-eager-annotation-start) otherwise it
 will be lost.
 
@@ -1018,7 +1052,11 @@ It is safe to leave this variable unset (as nil)."
 
 (defcustom proof-shell-proof-completed-regexp nil
   "Regexp matching output indicating a finished proof.
-Match number 1 should be the response text."
+Match number 1 should be the response text.
+
+This is used to enable the QED function (save a proof) and
+to control what output appears in the response buffer at the
+end of a proof."
   :type 'regexp
   :group 'proof-shell)
 
@@ -1037,7 +1075,10 @@ is shown to the user.  Set to nil to disable."
   :group 'proof-shell)
 
 (defcustom proof-shell-start-goals-regexp ""
-  "Regexp matching the start of the proof state output."
+  "Regexp matching the start of the proof state output.
+This is an important setting.  Output between `proof-shell-start-goals-regexp'
+and `proof-shell-end-goals-regexp' will be pasted into the goals buffer
+and possibly analysed further for proof-by-pointing markup."
   :type 'regexp
   :group 'proof-shell)
 
@@ -1154,7 +1195,7 @@ NB: You should be very careful about setting this hook.  Proof General
 relies on a careful synchronization with the process between inputs
 and outputs.  It expects to see a prompt for each input it sends from
 the queue.  If you add extra input here and it causes more prompts
-than expected, things will break!  Massaging the STRING variable
+than expected, things will break!  Massaging the variable STRING
 may be safer since it is stripped of carriage returns 
 before being sent."
   :type '(repeat function)
@@ -1162,7 +1203,7 @@ before being sent."
 
 (defcustom proof-pre-shell-start-hook nil
   "Hooks run before proof shell is started.
-This may be set to a function which configures the proof shell
+Suggestion: set this to a function which configures the proof shell
 variables."
   :type '(repeat function)
   :group 'proof-shell)
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 4b84afc3..98d0ce2c 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -429,10 +429,21 @@ to allow other files loaded by proof assistants to be marked read-only."
 		    :test 'equal)))
     (and pos (nth pos buffers))))
 
+;; FIXME da: cleanup of odd asymmetry here: we have a nice setting for
+;; proof-register-possibly-new-processed-file but something much more
+;; complicated for retracting, because we allow a hook function
+;; to calculate the new included files list.
+
 (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."
+to co-ordinate with its internal file-management.  (Otherwise we assume
+that it is a message from the proof assistant which triggers this call).
+
+No action is taken if the file is already registered.
+
+A warning message is issued if the register request came from the
+proof assistant and Emacs is has a modified buffer visiting the file."
   (let* ((cfile (file-truename file))
 	 (buffer (proof-file-to-buffer cfile)))
     (proof-debug (concat "Registering file " cfile 
@@ -440,6 +451,7 @@ to co-ordinate with its internal file-management."
 			     " (already registered, no action)." ".")))
     (unless (member cfile proof-included-files-list)
       (and buffer
+	   (not informprover)
 	   (buffer-modified-p buffer)
 	   (proof-warning (concat "Changes to "
 				  (buffer-name buffer)
@@ -452,20 +464,30 @@ to co-ordinate with its internal file-management."
       ;; Tell the proof assistant, if we should and if we can
       (if (and informprover proof-shell-inform-file-processed-cmd)
 	  (proof-shell-invisible-command 
-	   (format proof-shell-inform-file-processed-cmd cfile))))))
+	   (format proof-shell-inform-file-processed-cmd cfile) 
+	   'wait)))))
 
-(defun proof-unregister-buffer-file-name ()
+(defun proof-unregister-buffer-file-name (&optional informprover)
   "Remove current buffer's filename from the list of included files.
-No effect if the current buffer has no file name."
+No effect if the current buffer has no file name.
+If INFORMPROVER is non-nil,  the proof assistant will be told about this,
+using proof-shell-inform-file-retracted-cmd, to co-ordinate with its 
+internal file-management."
   (if buffer-file-name
       (let ((cfile (file-truename buffer-file-name)))
 	(proof-debug (concat "Unregistering file " cfile 
 			       (if (not (member cfile 
 						proof-included-files-list))
-				   " (not registered)." ".")))
-	(setq proof-included-files-list
-	      (delete cfile proof-included-files-list)))))
-
+				   " (not registered, no action)." ".")))
+	(if (member cfile proof-included-files-list)
+	    (progn
+	      (setq proof-included-files-list
+		    (delete cfile proof-included-files-list))
+	      ;; Tell the proof assistant, if we should and we can.
+	      (if (and informprover proof-shell-inform-file-retracted-cmd)
+		  (proof-shell-invisible-command
+		   (format proof-shell-inform-file-retracted-cmd cfile) 
+		   'wait)))))))
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -596,7 +618,13 @@ a scripting buffer is killed it is always retracted."
 	      
 	      (if (proof-locked-region-empty-p)
 		  ;; If locked region is empty, make sure this buffer is
-		  ;; *off* the included files list.  
+		  ;; *off* the included files list. 
+		  ;; FIXME: probably this isn't necessary: the
+		  ;; file should be unregistered by the retract
+		  ;; action, or in any case since it was only
+		  ;; partly processed.
+		  ;; We move the onus on unregistering now to
+		  ;; the activate-scripting action.
 		  (proof-unregister-buffer-file-name))
 
 	      ;; Turn off Scripting here.
@@ -669,6 +697,12 @@ correct theory, or whatever."
 	  ;; sometimes we switch on scripting in "full" buffers,
 	  ;; so mustn't do this.
 	  (proof-init-segmentation))
+
+      ;; Now make sure that this buffer is off the included files
+      ;; list.  In case we re-activate scripting in an already
+      ;; completed buffer, it may be that the proof assistant
+      ;; needs to retract some of this buffer's dependencies.
+      (proof-unregister-buffer-file-name 'tell-the-prover)
       
       ;; Turn on the minor mode, make it show up.
       (setq proof-active-buffer-fake-minor-mode t)