Add proof-shell-require-command-regexp, proof-done-advancing-require-function

to support multiple files in Coq.
Move some keybindings to proof-universal-keys (esp. C-c C-l).

3 files changed, 68 insertions, 13 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 5b8ae83d..b7bf3e7a 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1645,9 +1645,14 @@ also unlocked.
 
 If this is set to nil, no command is issued.
 
+It is also possible to set this value to a function which will
+be invoked on the name of the retracted file, and should remove 
+the ancestor files from `proof-included-files-list' by some
+other calculation.
+
 See also: proof-shell-inform-file-processed-cmd, 
 proof-shell-process-file, proof-shell-compute-new-files-list."
- :type '(choice string (const nil))
+ :type '(choice string (const nil)) ;; FIXME: or function
  :group 'proof-shell)
 
 (defcustom proof-auto-multiple-files nil
@@ -1679,6 +1684,24 @@ scripting (to do undo operations), the whole history is discarded."
   :type 'boolean
   :group 'proof-shell)  ;; not really proof shell
 
+(defcustom proof-shell-require-command-regexp nil
+  "A regular expression to match a Require-type of command, or nil.
+If set to a regexp, then `proof-done-advancing-require-function'
+should also be set, and will be called immediately after the match.
+
+This can be used to adjust `proof-included-files-list' based on the
+lines of script that have been processed/parsed, rather than relying
+on information from the prover."
+  :type 'regexp
+  :group 'proof-shell)
+
+(defcustom proof-done-advancing-require-function nil
+  "Invoked from `proof-done-advancing', see `proof-shell-require-command-regexp'.
+The function is passed the span and the command as arguments."
+  :type 'function
+  :group 'proof-shell)
+  
+
 ;; (defcustom  proof-shell-adjust-line-width-cmd nil
 
 
@@ -2585,6 +2608,11 @@ If this table is empty or needs adjusting, please make changes using
        '([(control c) \`] . proof-next-error)
      '("`" . proof-next-error))
    '(([(control c) (control c)] . proof-interrupt-process)
+     ([(control c) (control n)] . proof-assert-next-command-interactive)
+     ([(control c) (control u)] . proof-undo-last-successful-command)
+     ([(control c) (control p)] . proof-prf)
+     ([(control c) (control l)] . proof-layout-windows)
+     ([(control c) (control c)] . proof-interrupt-process)
      ([(control c) (control v)] . proof-minibuffer-cmd)
      ([(control c) (control w)] . pg-response-clear-displays)))
 "List of key-bindings made for the script, goals and response buffer. 
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index a6cfecd1..e1c59f2b 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -91,14 +91,14 @@ without adjusting window layout."
 ;; C-c C-c is proof-interrupt-process in universal-keys
 (define-key map [(control c) (control f)] 'proof-find-theorems)
 (define-key map [(control c) (control h)] 'proof-help)
+;; C-c C-l is proof-layout-windows in universal-keys
+;; C-c C-n is proof-assert-next-command-interactive in universal-keys
 (define-key map [(control c) (control o)] 'proof-display-some-buffers)
-(define-key map [(control c) (control l)] 'proof-layout-windows)
-(define-key map [(control c) (control n)] 'proof-assert-next-command-interactive)
 (define-key map [(control c) (control p)] 'proof-prf)
 (define-key map [(control c) (control r)] 'proof-retract-buffer)
 (define-key map [(control c) (control s)] 'proof-toggle-active-scripting)
 (define-key map [(control c) (control t)] 'proof-ctxt)
-(define-key map [(control c) (control u)] 'proof-undo-last-successful-command)
+;; C-c C-u is proof-undo-last-successful-command in universal-keys
 ;; C-c C-w is pg-response-clear-displays in universal-keys
 (define-key map [(control c) (control z)] 'proof-frob-locked-end)
 (define-key map [(control c) (control backspace)] 'proof-undo-and-delete-last-successful-command)
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 4369adfd..efe17747 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -809,11 +809,23 @@ proof assistant and Emacs has a modified buffer visiting the file."
 	     'wait))))))
 
 (defun proof-inform-prover-file-retracted (rfile)
-  (if proof-shell-inform-file-retracted-cmd
-      (proof-shell-invisible-command
-       (proof-format-filename proof-shell-inform-file-retracted-cmd
-			      rfile)
-       'wait)))
+  (cond
+   ((stringp proof-shell-inform-file-retracted-cmd)
+    (proof-shell-invisible-command
+     (proof-format-filename proof-shell-inform-file-retracted-cmd
+			    rfile)
+     'wait))
+   ;; If it's a function it might not actually be informing the prover at all,
+   ;; but merely cleans up proof-included-files-list by its own magic.  We
+   ;; do the same thing as in proof-shell.el.  
+   ;; FIXME: clean and amalgamate this code.
+   ((functionp proof-shell-inform-file-retracted-cmd)
+    (let ((current-included proof-included-files-list))
+      (funcall proof-shell-inform-file-retracted-cmd rfile)
+      (proof-restart-buffers
+       (proof-files-to-buffers
+	(set-difference current-included
+			proof-included-files-list)))))))
 
 (defun proof-auto-retract-dependencies (cfile &optional informprover)
   "Perhaps automatically retract the (linear) dependencies of CFILE.
@@ -1317,10 +1329,25 @@ With ARG, turn on scripting iff ARG is positive."
 	     (and (eq proof-completed-proof-behaviour 'closegoal)
 		  (funcall proof-goal-command-p cmd))))
 	(proof-done-advancing-autosave span))
-      
-     ;; CASE 4:  Some other kind of command (or a nested goal).
-     (t
-      (proof-done-advancing-other span))))
+
+       ;; CASE 4: A "Require" type of command is seen (Coq).
+       ;; 
+       ((and 
+	 proof-shell-require-command-regexp
+	 (proof-string-match proof-shell-require-command-regexp cmd))
+	;; We take additional action dependent on prover
+	;; [FIXME: use same method as in proof-shell here to
+	;;  recompute proof-included-files and adjust it]
+	;; FIXME 2: we could annotate the Require ourselves
+	;; at this point to contain the buffers which are
+	;; being included!  Then undoing can retract them.
+	(funcall proof-done-advancing-require-function span cmd)
+	;; But do what we would have done anyway
+	(proof-done-advancing-other span))
+       
+       ;; CASE 5:  Some other kind of command (or a nested goal).
+       (t
+	(proof-done-advancing-other span))))
 
   ;; Finally: state of scripting may have changed now, run hooks.
   (run-hooks 'proof-state-change-hook)))