Add preliminary support for multiple files for coq.

The following points are implemented already:
- recompile either via an external command (make) or let
  ProofGeneral handle everything internally
- complete dependency tracking and recompilation for coq files in
  internal mode
- support for extending the LoadPath: does almost work, even if
  specified file-locally
- move back to clean state if recompilation fails

There are the following known problems:
- coq-load-path extensions are not retracted
- fails on partially qualified library names

4 files changed, 50 insertions, 11 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index cd41084a..f93235d4 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1539,6 +1539,14 @@ if you don't need it (slight speed penalty)."
   :type 'boolean
   :group 'proof-shell)
 
+(defcustom proof-shell-extend-queue-hook nil
+  "Hooks run by proof-extend-queue before extending `proof-action-list'.
+Can be used to run additional actions before items are added to the queue
+\(such as recompiling required modules for Coq) or to modify the items
+that are going to be added to `proof-action-list'."
+  :type '(repeat function)
+  :group 'proof-shell)  
+
 (defcustom proof-shell-insert-hook nil
   "Hooks run by `proof-shell-insert' before inserting a command.
 Can be used to configure the proof assistant to the interface in
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 89c53d65..2c2c760d 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -969,6 +969,14 @@ retracted using `proof-auto-retract-dependencies'."
 ;; taken when scripting is turned off/on.
 ;;
 
+(defconst proof-no-fully-processed-buffer nil
+  "Set to t if buffers should always retract before scripting elsewhere.
+Leave at nil if fully processd buffers make sense for the current proof
+assistant. If nil the user can choose to fully assert a buffer when
+starting scripting in a different buffer. If t there is only to choice
+to fully retract the active buffer before starting scripting in a different
+buffer. This last behavior is needed for Coq.")
+
 (defun proof-protected-process-or-retract (action &optional buffer)
   "If ACTION='process, process, If ACTION='retract, retract.
 Process or retract the current buffer, which should be the active
@@ -1015,7 +1023,13 @@ We make sure that the active scripting buffer either has no locked
 region or a full locked region (everything in it has been processed).
 If this is not already the case, we question the user whether to
 retract or assert, or automatically take the action indicated in the
-user option `proof-auto-action-when-deactivating-scripting.'
+user option `proof-auto-action-when-deactivating-scripting'.
+
+If `proof-no-fully-processed-buffer' is t there is only the choice
+to fully retract the active scripting buffer. In this case the
+active scripting buffer is retract even if it was fully processed.
+Setting `proof-auto-action-when-deactivating-scripting' to 'process
+is ignored in this case.
 
 If the scripting buffer is (or has become) fully processed, and it is
 associated with a file, it is registered on
@@ -1047,13 +1061,18 @@ a scripting buffer is killed it is always retracted."
 	;; switching between buffers during a proof makes
 	;; no sense.)
 	(if (or (proof-locked-region-empty-p)
-		(proof-locked-region-full-p)
+		(and (not proof-no-fully-processed-buffer)
+		     (proof-locked-region-full-p))
 		;; Buffer is partly-processed
 		(let*
-		    ((action
-		      (or
-		       forcedaction
-		       proof-auto-action-when-deactivating-scripting
+		    ((auto-action
+		      (if (and proof-no-fully-processed-buffer
+			       (eq proof-auto-action-when-deactivating-scripting
+				   'process))
+			  nil
+			proof-auto-action-when-deactivating-scripting))
+		     (action
+		      (or forcedaction auto-action
 		       (progn
 			 (save-window-excursion
 			   (unless
@@ -1078,10 +1097,12 @@ a scripting buffer is killed it is always retracted."
 			       "Scripting incomplete in buffer %s, retract? "
 			       proof-script-buffer))
 			     'retract)
-			    ((y-or-n-p
-			      (format
-			       "Completely process buffer %s instead? "
-			       proof-script-buffer))
+			    ((and
+			      (not proof-no-fully-processed-buffer)
+			      (y-or-n-p
+			       (format
+				"Completely process buffer %s instead? "
+				proof-script-buffer)))
 			     'process)))))))
 		  ;; Take the required action
 		  (if action
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 0c0b2173..a09ddd78 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -924,6 +924,11 @@ To make sense, the commands should correspond to processing actions
 for processing a region from (buffer-queue-or-locked-end) to END.
 The queue mode is set to 'advancing"
   (proof-set-queue-endpoints (proof-unprocessed-begin) end)
+  (condition-case err
+      (run-hooks 'proof-shell-extend-queue-hook)
+    (error
+     (proof-detach-queue)
+     (signal (car err) (cdr err))))
   (proof-add-to-queue queueitems 'advancing))
 
 
diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el
index 1a141741..b58228c2 100644
--- a/generic/proof-useropts.el
+++ b/generic/proof-useropts.el
@@ -314,7 +314,12 @@ makes sense within the proof assistant.
 
 NB: A buffer is completely processed when all non-whitespace is
 locked (coloured blue); a buffer is completely unprocessed when there
-is no locked region."
+is no locked region.
+
+For some proof assistants (such as Coq) fully processed buffers make
+no sense. Setting this option to 'process has then the same effect
+as leaving it unset (nil). (This behaviour is controlled by
+`proof-no-fully-processed-buffer'.)"
   :type '(choice
 	  (const :tag "No automatic action; query user" nil)
 	  (const :tag "Automatically retract" retract)