- fix broken external compilation

- fix quitting during compilation
- substitute "compile" for "recompile"
- added documentation

3 files changed, 460 insertions, 122 deletions

diff --git a/coq/coq.el b/coq/coq.el
index 3dad1fa7..0a8ec0ed 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1092,74 +1092,82 @@ Currently this doesn't take the loadpath into account."
 ;;
 
 ;; TODO list:
-;; - work through comments on the first patch
-;; - fix condition-case in error messages
-;; - testcases & examples
 ;; - display coqdep errors in the recompile-response buffer
 ;; - use a variable for the recompile-response buffer
 ;; - fix problem with partial library names
 ;; - clean old multiple file stuff
-;; - write docs
 ;; - fix places marked with XXX
 ;; - test and fix problems when switchen scripting between different directories
 ;; - enable next-error in recompile-response buffers
+;; - call compile more cleverly, with a coq-specific option for compile
+;;   command confirmation
 
 ;; user options and variables
 
-(defgroup coq-auto-recompile ()
-  "Customization for automatic recompilation of required files"
+(defgroup coq-auto-compile ()
+  "Customization for automatic compilation of required files"
   :group 'coq
   :package-version '(ProofGeneral . "4.1"))
 
-(defcustom coq-recompile-before-require t
-  "If `t' check dependencies of required modules and recompile if necessary.
+(defcustom coq-compile-before-require t
+  "*If `t' check dependencies of required modules and compile if necessary.
 If `t' ProofGeneral intercepts \"Require\" commands and checks if the
 required library module and its dependencies are up-to-date. If not, they
-are recompiled from the sources before the \"Require\" command is processed."
+are compiled from the sources before the \"Require\" command is processed."
   :type 'boolean
-  :group 'coq-auto-recompile)
+  :group 'coq-auto-compile)
 
-(defcustom coq-recompile-command ""
-  "External recompilation command. If empty ProofGeneral recompiles itself.
+(defcustom coq-compile-command ""
+  "*External compilation command. If empty ProofGeneral compiles itself.
 If unset (the empty string) ProofGeneral computes the dependencies of
-required modules with coqdep and recompiles as necessary. This internal
+required modules with coqdep and compiles as necessary. This internal
 dependency checking does currently not handle ML modules.
 
 If a non-empty string, the denoted command is called to do the dependency
-checking and recompilation. Before calling this command via `compile'
+checking and compilation. Before calling this command via `compile'
 the following keys are substituted as follows:
-  %p  the (physical) directory containing the required module
-  %m  the name of the required module (without extension or directory part)
-  %f  the file containing the Require command
-  %l  the logical path of the required module
-      (or \"<>\" for the empty logical path)
-
-For instance, \"make -C %p %m.vo\" expands to \"make -C bar foo.vo\"
+  %p  the (physical) directory containing the source of
+      the required module
+  %o  the coq object file in the physical directory that will
+      be loaded
+  %q  the qualified id of the \"Require\" command
+  %r  the source file containing the \"Require\"
+
+For instance, \"make -C %p %o\" expands to \"make -C bar foo.vo\"
 when module \"foo\" from directory \"bar\" is required."
   :type 'string
-  :group 'coq-auto-recompile)
+  :group 'coq-auto-compile)
 
-(defconst coq-recompile-substitution-list
+(defconst coq-compile-substitution-list
   '(("%p" physical-dir)
-    ("%m" module)
-    ("%f" requiring-file)
-    ("%l" logical-dir))
-  "Substitutions for `coq-recompile-command'.
-Value must be a list of substitutions, where each substitution is a 2-element
-list. The first element of a substitution is the regexp to substitute, the
-second the replacement. The replacement is evaluated before passing it to
-`replace-regexp-in-string', so it might be a string, or one of the symbols
-'module, 'physical-dir, 'requiring-file, and 'logical-dir, which are bound,
-respectively, to the required module (without directory part), the physical
- directory containing it, the file containing the Require command, and the
-logical path specified in the Require command.")
-
-(defcustom coq-recompile-auto-save 'ask-coq
-  "Buffers to save before checking dependencies for recompilation.
+    ("%o" module-object)
+    ("%q" qualified-id)
+    ("%r" requiring-file))
+  "Substitutions for `coq-compile-command'.
+Value must be a list of substitutions, where each substitution is
+a 2-element list. The first element of a substitution is the
+regexp to substitute, the second the replacement. The replacement
+is evaluated before passing it to `replace-regexp-in-string', so
+it might be a string, or one of the symbols 'physical-dir,
+'module-object, 'qualified-id and 'requiring-file, which are
+bound, respectively, to the the physical directory containing the
+source file, the Coq object file in 'physical-dir that will be
+loaded, the qualified module identifier that occurs in the
+\"Require\" command, and the file that contains the
+\"Require\".")
+
+(defcustom coq-compile-auto-save 'ask-coq
+  "*Buffers to save before checking dependencies for compilation.
 There are two orthogonal choices: Firstly one can save all or only the coq
 buffers, where coq buffers means all buffers in coq mode except the current
 buffer. Secondly, emacs can ask about each such buffer or save all of them
-unconditionally."
+unconditionally.
+
+This makes four permitted values: 'ask-coq to confirm saving all
+modified Coq buffers, 'ask-all to confirm saving all modified
+buffers, 'save-coq to save all modified Coq buffers without
+confirmation and 'save-all to save all modified buffers without
+confirmation."
   :type
   '(radio
     (const :tag "ask for each coq-mode buffer, except the current buffer"
@@ -1170,28 +1178,33 @@ unconditionally."
      "save all coq-mode buffers except the current buffer without confirmation"
      save-coq)
     (const :tag "save all buffers without confirmation" save-all))
-  :group 'coq-auto-recompile)
+  :group 'coq-auto-compile)
 
-(defcustom coq-recompile-ignore-library-directory t
-  "If `t' ProofGeneral does not recompile modules from the coq library.
+(defcustom coq-compile-ignore-library-directory t
+  "*If `t' ProofGeneral does not compile modules from the coq library.
 Should be `t' for normal coq users. If `nil' library modules are
-recompiled if their sources are newer."
+compiled if their sources are newer.
+
+This option has currently no effect, because Proof General uses
+coqdep to translate qualified identifiers into library file names
+and coqdep does not output dependencies in the standard library."
   :type 'boolean
-  :group 'coq-auto-recompile)
-
-(defcustom coq-recompile-ignored-directories nil
-  "Directories in which ProofGeneral should not recompile modules.
-List of regular expressions for directories in which ProofGeneral should
-not recompile modules. If a file name matches one of the regular expressions
-in this list then ProofGeneral does neither recompile this file nor check
-its dependencies for recompilation. It makes sense to include non-standard
-coq library directories here if they are not changed and if they are so big
+  :group 'coq-auto-compile)
+
+(defcustom coq-compile-ignored-directories nil
+  "*Directories in which ProofGeneral should not compile modules.
+List of regular expressions for directories in which ProofGeneral
+should not compile modules. If a library file name matches one
+of the regular expressions in this list then ProofGeneral does
+neither compile this file nor check its dependencies for
+compilation. It makes sense to include non-standard coq library
+directories here if they are not changed and if they are so big
 that dependency checking takes noticeable time."
   :type '(repeat regexp)
-  :group 'coq-auto-recompile)
+  :group 'coq-auto-compile)
 
 (defcustom coq-load-path nil
-  "Non-standard coq library load path.
+  "*Non-standard coq library load path.
 List of directories to be added to the LoadPath of coqdep, coqc
 and coqtop. Under normal circumstances this list does not need to
 contain \".\" for the current directory (see
@@ -1202,15 +1215,15 @@ For coqdep and coqc these directories are passed via \"-I\"
 options over the command line. For interactive scripting an
 \"Add LoadPath\" command is used."
   :type '(repeat string)
-  :group 'coq-auto-recompile)
+  :group 'coq-auto-compile)
 
 (defcustom coq-load-path-include-current t
-  "If `t' let coqdep search the current directory too.
+  "*If `t' let coqdep search the current directory too.
 Should be `t' for normal users. If `t' pass \"-I dir\" to coqdep when
 processing files in directory \"dir\" in addition to any entries
 in `coq-load-path'."
   :type 'boolean
-  :group 'coq-auto-recompile)
+  :group 'coq-auto-compile)
 
 (defconst coq-require-command-regexp
   "^Require[ \t\n]+\\(Import\\|Export\\)?[ \t\n]*"
@@ -1249,15 +1262,15 @@ For time values see `time-less'."
 (defun coq-max-dep-mod-time (dep-mod-times)
   "Return the maximum in DEP-MOD-TIMES.
 Argument DEP-MOD-TIMES is a list where each element is either a
-time value (see `time-less') or 'just-recompiled. The
+time value (see `time-less') or 'just-compiled. The
 function returns the maximum of the elements in DEP-MOD-TIMES,
-where 'just-recompiled is considered the greatest time value. If
+where 'just-compiled is considered the greatest time value. If
 DEP-MOD-TIMES is empty it returns nil."
   (let ((max nil))
     (while dep-mod-times
       (cond
-       ((eq (car dep-mod-times) 'just-recompiled)
-        (setq max 'just-recompiled
+       ((eq (car dep-mod-times) 'just-compiled)
+        (setq max 'just-compiled
               dep-mod-times nil))
        ((eq max nil)
         (setq max (car dep-mod-times)))
@@ -1276,15 +1289,15 @@ DEP-MOD-TIMES is empty it returns nil."
 
 ;; handle Require commands when queue is extended
 
-(defun coq-recompile-ignore-file (lib-obj-file)
-  "Check whether ProofGeneral should handle recompilation of LIB-OBJ-FILE.
+(defun coq-compile-ignore-file (lib-obj-file)
+  "Check whether ProofGeneral should handle compilation of LIB-OBJ-FILE.
 Return `t' if ProofGeneral should skip LIB-OBJ-FILE and `nil' if
 ProofGeneral should handle the file. For normal users it does, for instance,
 not make sense to let ProofGeneral check if the coq standard library
 is up-to-date."
   (or
    (and
-    coq-recompile-ignore-library-directory
+    coq-compile-ignore-library-directory
     (eq (compare-strings coq-library-directory 0 nil
                          lib-obj-file 0 (length coq-library-directory))
         t)
@@ -1292,7 +1305,7 @@ is up-to-date."
     t)
    (if (some
         (lambda (dir-regexp) (string-match dir-regexp lib-obj-file))
-        coq-recompile-ignored-directories)
+        coq-compile-ignored-directories)
        (message "Ignore %s" lib-obj-file) ;XXX
      nil)))
 
@@ -1349,11 +1362,11 @@ break."
           (cdr-safe (split-string (match-string 1 coqdep-output)))
         ()))))
 
-(defun coq-recompile-library (src-file)
+(defun coq-compile-library (src-file)
   "Recompile coq library SRC-FILE.
-Display errors in buffer *coq-auto-recompile-response*."
+Display errors in buffer *coq-auto-compile-response*."
   (message "Recompile %s" src-file)
-  (with-current-buffer (get-buffer-create "*coq-auto-recompile-response*")
+  (with-current-buffer (get-buffer-create "*coq-auto-compile-response*")
     (erase-buffer))
   (let ((coqc-arguments
          (nconc (coq-include-options src-file) (list src-file)))
@@ -1361,7 +1374,7 @@ Display errors in buffer *coq-auto-recompile-response*."
     ;(message "call coqc arg list: %s" coqc-arguments)
     (setq coqc-status
           (apply 'call-process
-           coq-compiler nil "*coq-auto-recompile-response*" t coqc-arguments))
+           coq-compiler nil "*coq-auto-compile-response*" t coqc-arguments))
     ; (if (eq coqc-status 0)
     ;     (message "compilation %s OK, output |%s|" src-file
     ;              (with-current-buffer proof-response-buffer
@@ -1371,35 +1384,35 @@ Display errors in buffer *coq-auto-recompile-response*."
              (if (numberp coqc-status)
                  "terminated with exit status"
                "was terminated by signal")))
-        (display-buffer "*coq-auto-recompile-response*")
+        (display-buffer "*coq-auto-compile-response*")
         (error "ERROR: Recompiling coq library %s %s %s"
                src-file terminated-text coqc-status)))))
 
-(defun coq-recompile-library-if-necessary (max-dep-obj-time src obj)
+(defun coq-compile-library-if-necessary (max-dep-obj-time src obj)
   "Recompile SRC to OBJ if necessary.
-This function recompiles SRC to the coq library object file OBJ
+This function compiles SRC to the coq library object file OBJ
 if one of the following conditions is true:
-- a dependency has just been recompiled
+- a dependency has just been compiled
 - OBJ does not exist
 - SRC is newer than OBJ
 - OBJ is older than the the youngest object file of the dependencies.
 
 Argument MAX-DEP-OBJ-TIME provides the information about the
 dependencies. It is either
-- 'just-recompiled if one of the dependencies of SRC has just
+- 'just-compiled if one of the dependencies of SRC has just
   been compiled
 - the time value (see`time-less') of the youngest (most recently
   created) object file among the dependencies
 - nil if there are no dependencies, or if they are all ignored
 
 If this function decides to compile SRC to OBJ it returns
-'just-recompiled. Otherwise it returns the modification time of
+'just-compiled. Otherwise it returns the modification time of
 OBJ."
   (let (src-time obj-time)
-    (if (eq max-dep-obj-time 'just-recompiled)
+    (if (eq max-dep-obj-time 'just-compiled)
         (progn
-          (coq-recompile-library src)
-          'just-recompiled)
+          (coq-compile-library src)
+          'just-compiled)
       (setq src-time (nth 5 (file-attributes src)))
       (setq obj-time (nth 5 (file-attributes obj)))
       (if (or
@@ -1410,8 +1423,8 @@ OBJ."
                                         ; which is newer than obj
             (time-less-or-equal obj-time max-dep-obj-time)))
           (progn
-            (coq-recompile-library src)
-            'just-recompiled)
+            (coq-compile-library src)
+            'just-compiled)
         (message "Skip compilation of %s" src) ; XXX
         obj-time))))
 
@@ -1419,7 +1432,7 @@ OBJ."
   "Make library object file LIB-OBJ-FILE up-to-date.
 Check if LIB-OBJ-FILE and all it dependencies are up-to-date
 compiled coq library objects. Recompile the necessary objects, if
-not. This function returns 'just-compiled if it recompiled
+not. This function returns 'just-compiled if it compiled
 LIB-OBJ-FILE. Otherwise it returns the modification time of
 LIB-OBJ-FILE as time value (see `time-less').
 
@@ -1435,7 +1448,7 @@ function."
           result)
       ;; lib-obj-file has not been check -- do it now
       (message "Check %s" lib-obj-file)     ;XXX
-      (if (coq-recompile-ignore-file lib-obj-file)
+      (if (coq-compile-ignore-file lib-obj-file)
           ;; return minimal time for ignored files
           (setq result '(0 0))
         (let* ((lib-src-file
@@ -1453,7 +1466,7 @@ function."
                          (coq-make-lib-up-to-date coq-obj-hash dep))
                        dependencies))
                 (setq result
-                      (coq-recompile-library-if-necessary
+                      (coq-compile-library-if-necessary
                        (coq-max-dep-mod-time deps-mod-time)
                        lib-src-file lib-obj-file)))
             (message "coq-auto-compile: no source file for %s" lib-obj-file)
@@ -1465,28 +1478,28 @@ function."
       (puthash lib-obj-file result coq-obj-hash)
       result)))
 
-(defun coq-auto-recompile-externally (requiring-file logical-dir
-                                                      physical-dir module)
-  "Make MODULE up-to-date according to `coq-recompile-command'.
+(defun coq-auto-compile-externally (qualified-id absolute-module-obj-file)
+  "Make MODULE up-to-date according to `coq-compile-command'.
 Call `compile' to make MODULE up-to-date. The compile command is derived
-from `coq-recompile-command' by substituting certain keys, see
-`coq-recompile-command' for details. Customizing `compile-command' has
-therefore no effect, customize `coq-recompile-command' instead. All other
+from `coq-compile-command' by substituting certain keys, see
+`coq-compile-command' for details. Customizing `compile-command' has
+therefore no effect, customize `coq-compile-command' instead. All other
 customizations of `compile' apply, so set the variable
 `compilation-read-command' to nil if you don't want to confirm the
-recompilation command. Further, `compilation-ask-about-save' to nil
-to save all buffers without confirmation before recompilation."
-  (unless (coq-recompile-ignore-file (concat physical-dir "/" module ".vo"))
-    (let ((compile-command coq-recompile-command))
-      (if (equal logical-dir "")
-          (setq logical-dir "<>"))
+compilation command. Further, set `compilation-ask-about-save' to nil
+to save all buffers without confirmation before compilation."
+  (unless (coq-compile-ignore-file absolute-module-obj-file)
+    (let ((compile-command coq-compile-command)
+          (physical-dir (file-name-directory absolute-module-obj-file))
+          (module-object (file-name-nondirectory absolute-module-obj-file))
+          (requiring-file buffer-file-name))
       (mapc
        (lambda (substitution)
          (setq compile-command
                (replace-regexp-in-string
                 (car substitution) (eval (car (cdr substitution)))
                 compile-command)))
-       coq-recompile-substitution-list)
+       coq-compile-substitution-list)
       (call-interactively 'compile))))
 
 (defun coq-map-module-id-to-obj-file (module-id)
@@ -1518,31 +1531,31 @@ function returns () if MODULE-ID comes from the standard library."
     (car-safe result)))
 
 (defun coq-check-module (coq-object-local-hash-symbol module-id)
-  "Locate MODULE-ID and recompile if necessary.
-If `coq-recompile-command' is not nil the whole task of checking which
-modules need recompilation and the recompilation itself is done by an external
-process. If `coq-recompile-command' is nil ProofGeneral computes the
+  "Locate MODULE-ID and compile if necessary.
+If `coq-compile-command' is not nil the whole task of checking which
+modules need compilation and the compilation itself is done by an external
+process. If `coq-compile-command' is nil ProofGeneral computes the
 dependencies with \"coqdep\" and compiles modules as necessary. This internal
 checking does currently not handle ML modules.
 
 Argument COQ-OBJECT-LOCAL-HASH-SYMBOL provides a place to store
 the coq-obj-hash, which is used during internal
-recompilation (see `coq-make-lib-up-to-date'). This way one hash
+compilation (see `coq-make-lib-up-to-date'). This way one hash
 will be used for all \"Require\" commands added at once to the
 queue."
-  (let ((module-file (coq-map-module-id-to-obj-file module-id)))
+  (let ((module-obj-file (coq-map-module-id-to-obj-file module-id)))
     ;; coq-map-module-id-to-obj-file currently returns () for
     ;; standard library modules!
-    (when module-file
-      (if (> (length coq-recompile-command) 0)
-          (coq-auto-recompile-externally module-file)
+    (when module-obj-file
+      (if (> (length coq-compile-command) 0)
+          (coq-auto-compile-externally module-id module-obj-file)
         (unless (symbol-value coq-object-local-hash-symbol)
           (set coq-object-local-hash-symbol (make-hash-table :test 'equal)))
         (coq-make-lib-up-to-date (symbol-value coq-object-local-hash-symbol)
-                                 module-file)))))
+                                 module-obj-file)))))
 
-(defun coq-recompile-save-buffer-filter ()
-  "Filter predicate for `coq-recompile-save-some-buffers'.
+(defun coq-compile-save-buffer-filter ()
+  "Filter predicate for `coq-compile-save-some-buffers'.
 See also `save-some-buffers'. Returns t for buffers with major mode
 'coq-mode' different from coq-process-require-current-buffer and nil
 for all other buffers. The buffer to test must be current."
@@ -1551,33 +1564,33 @@ for all other buffers. The buffer to test must be current."
    (not (eq coq-process-require-current-buffer
             (current-buffer)))))
   
-(defun coq-recompile-save-some-buffers ()
-  "Save buffers according to `coq-recompile-auto-save'.
+(defun coq-compile-save-some-buffers ()
+  "Save buffers according to `coq-compile-auto-save'.
 Uses the local variable coq-process-require-current-buffer to pass the
 current buffer (which contains the Require command) to
-`coq-recompile-save-buffer-filter'."
+`coq-compile-save-buffer-filter'."
   (let ((coq-process-require-current-buffer (current-buffer))
         unconditionally buffer-filter)
     (cond
-     ((eq coq-recompile-auto-save 'ask-coq)
+     ((eq coq-compile-auto-save 'ask-coq)
       (setq unconditionally nil
-            buffer-filter 'coq-recompile-save-buffer-filter))
-     ((eq coq-recompile-auto-save 'ask-all)
+            buffer-filter 'coq-compile-save-buffer-filter))
+     ((eq coq-compile-auto-save 'ask-all)
       (setq unconditionally nil
             buffer-filter nil))
-     ((eq coq-recompile-auto-save 'save-coq)
+     ((eq coq-compile-auto-save 'save-coq)
       (setq unconditionally t
-            buffer-filter 'coq-recompile-save-buffer-filter))
-     ((eq coq-recompile-auto-save 'save-all)
+            buffer-filter 'coq-compile-save-buffer-filter))
+     ((eq coq-compile-auto-save 'save-all)
       (setq unconditionally t
             buffer-filter nil)))
     (save-some-buffers unconditionally buffer-filter)))
 
 (defun coq-preprocess-require-commands ()
   "Coq function for `proof-shell-extend-queue-hook'.
-If `coq-recompile-before-require' it t this function performs the
-recompilation (if necessary) of the dependencies."
-  (if coq-recompile-before-require
+If `coq-compile-before-require' it t this function performs the
+compilation (if necessary) of the dependencies."
+  (if coq-compile-before-require
       (let ((items queueitems)
             (previous-head nil)
             ;; coq-object-hash-symbol serves as a pointer to the
@@ -1594,7 +1607,7 @@ recompilation (if necessary) of the dependencies."
           (when (and string
                      (string-match coq-require-command-regexp string))
             (let ((start (match-end 0)))
-              (coq-recompile-save-some-buffers)
+              (coq-compile-save-some-buffers)
               ;; now process all required modules
               (while (string-match coq-require-id-regexp string start)
                 (setq start (match-end 0))
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index a8cf718d..98dc87ae 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -3430,6 +3430,11 @@ 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.
 
+For some proof assistants (such as Coq) fully processed buffers make
+no sense. Setting this option to @code{'process} has then the same effect
+as leaving it unset (nil). (This behaviour is controlled by
+@samp{@code{proof-no-fully-processed-buffer}}.)
+
 The default value is @code{nil}.
 @end defopt
 
@@ -3916,6 +3921,7 @@ assistant.  It supports most of the generic features of Proof General.
 
 @menu
 * Coq-specific commands::
+* Multiple File Support::
 * Editing multiple proofs::
 * User-loaded tactics::
 * Holes feature::
@@ -3945,6 +3951,325 @@ Prompts for a SearchIsos argument.
 @end table
 
 
+@node Multiple File Support
+@section Multiple File Support
+
+Since version 4.1 Coq Proof General has multiple file support. It
+consists of the following points:
+
+@table @asis
+@item Restarting @code{coqtop} when changing the active scripting buffer
+Different buffers may require different load path' or different
+sets of @code{-I} options. Because Coq cannot undo changes in the
+load path, Proof General is forced to restart @code{coqtop} when
+the active scripting buffer changes.
+@item Locking ancestors
+Locking those buffers on which the current active scripting
+buffer depends. This is controlled by the user option
+@code{coq-lock-ancestors}, 
+@ref{Customizing Coq Multiple File Support} and 
+@ref{Locking Ancestors}.
+@item (Re-)Compilation 
+Before a @code{Require} command is processed it may be necessary
+to save and compile some buffers. Because this feature
+conflicts with existing customization habits, it is switched off
+by default. When it is properly configured, one can freely switch
+between different buffers. Proof General will compile the
+necessary files whenever a @code{Require} command is processed. 
+
+The compilation feature does currently not support ML modules.
+@end table
+
+To enable the automatic compilation feature there are three
+points to adhere to:
+
+@itemize @bullet
+@item
+The option @code{coq-compile-before-require} must be
+turned on.
+@item 
+Nonstandard load path elements @emph{must} be configured in the
+option @code{coq-load-path}. @code{-I} options in
+@code{coq-prog-name} or @code{coq-prog-args} must be deleted.
+@item
+For a nonstandard compilation procedure and limited ML module
+support, @code{coq-compile-command} can be set to an external
+compilation command. For standard dependency analysis with
+@code{coqdep} and compilation with @code{coqc} the option
+@code{coq-compile-command} can be left empty. If this option is
+empty Proof General calls @code{coqdep} and @code{coqc} as
+needed.
+@end itemize
+
+
+
+@menu
+* Automatic Compilation in Detail::
+* Locking Ancestors::
+* Customizing Coq Multiple File Support::
+@end menu
+
+
+@node Automatic Compilation in Detail
+@subsection Automatic Compilation in Detail
+
+When @code{coq-compile-before-require} is enabled, Proof
+General looks for @code{Require} commands in text that gets
+asserted (i.e., in text that is moved from the editing region to
+the queue region, @ref{Locked queue and editing regions}). If
+Proof General finds a @code{Require} command, it checks the
+dependencies and (re-)compiles files as necessary. Only after
+this compilation is finished, Proof General starts sending the
+asserted text to the Coq process.
+
+@code{Declare ML Module} commands are currently not recognized.
+
+Proof General uses @code{coqdep} in order to translate the
+qualified identifiers in @code{Require} commands to coq library
+file names. Therefore @code{Require Arith} works, while
+@code{Require Arith.Le} gives an error. This is also the reason
+why nonstandard load path elements must be configured in
+@code{coq-load-path}. 
+
+Once the library file name has been determined, its dependencies
+must be checked and out-of-date files must be compiled. This can
+either be done internally, by Proof General itself, or by an
+external command. If @code{coq-compile-command} is the empty
+string, Proof General does dependency checking and compilation
+itself. Otherwise the command in @code{coq-compile-command} is
+started as an external process after substituting certain keys,
+@ref{Customizing Coq Multiple File Support}. 
+
+If Proof General uses an external command for compilation, this
+command is started via @code{compile}, @ref{Compilation,,,emacs}.
+Because Proof General cannot know if some library files have been
+updated outside of Proof General, it must perform the dependency
+checking for each @code{Require} command. The continuous
+confirmation of the external compilation commands can soon become
+tedious. Set @code{compilation-read-command} to nil to disable
+command confirmation for all invocations of @code{compile}, see
+the documentation of @code{compile} (which is displayed after
+typing C-h f compile). 
+
+When a @code{Require} command causes a compilation of some files
+one may wish to save some buffers to disk beforehand. The option
+@code{coq-compile-auto-save} controls how and which files are
+saved. There are two orthogonal choices: One may wish to save all
+or only the Coq source files, and, one may or may not want to
+confirm the saving of each file. 
+
+
+@node Locking Ancestors
+@subsection Locking Ancestors
+
+
+Locking ancestor files works as a side effect of the dependency
+checking. This means that ancestor locking does only work when
+Proof General performs dependency checking and compilation
+itself. If an external command is used, Proof General does not see
+the dependencies and can therefore not lock them. With external
+compilation only the direct ancestors are locked.
+
+Proof General's file locking machinery is at the moment only suited
+for source code processing proof assistants, such as Isabelle.
+Therefore locking ancestor files might not exactly do what Coq
+users expect. You can switch ancestor locking off by setting
+@code{coq-lock-ancestors} to nil, @ref{Customizing Coq Multiple
+File Support}. 
+
+Currently, when you want to edit a locked ancestor, you are
+forced to completely retract the current scripting buffer. The
+right behaviour for Coq would be to retract the current scripting
+buffer only up to the point before the appropriate @code{Require}
+command. At the users choice it should also be possible to unlock
+the ancestor without retracting the current scripting buffer. The
+latter would be adequate, if you just want to add a lemma in the
+ancestor @emph{and} want to continue the development in the
+current scripting buffer without interruption.
+
+
+
+@node Customizing Coq Multiple File Support
+@subsection Customizing Coq Multiple File Support
+
+The customization setting for multiple file support of Coq Proof
+General are in a separate customization group, the
+@code{coq-auto-compile} group. To view all options in this
+group do @code{M-x customize-group coq-auto-compile} or select
+menu entry @code{Proof-General -> Advanced -> Customize -> Coq ->
+Coq Auto Compile -> Coq Auto Compile}. 
+
+
+@c TEXI DOCSTRING MAGIC: coq-compile-before-require
+@defopt coq-compile-before-require 
+If @samp{t} check dependencies of required modules and compile if necessary.@*
+If @samp{t} ProofGeneral intercepts "Require" commands and checks if the
+required library module and its dependencies are up-to-date. If not, they
+are compiled from the sources before the "Require" command is processed.
+
+The default value is @code{t}.
+@end defopt
+
+
+@c TEXI DOCSTRING MAGIC: coq-compile-command
+@defopt coq-compile-command 
+External compilation command. If empty ProofGeneral compiles itself.@*
+If unset (the empty string) ProofGeneral computes the dependencies of
+required modules with coqdep and compiles as necessary. This internal
+dependency checking does currently not handle ML modules.
+
+If a non-empty string, the denoted command is called to do the dependency
+checking and compilation. Before calling this command via @samp{compile}
+the following keys are substituted as follows:
+@lisp
+  %p  the (physical) directory containing the source of
+      the required module
+  %o  the coq object file in the physical directory that will
+      be loaded
+  %q  the qualified id of the "Require" command
+  %r  the source file containing the "Require"
+@end lisp
+For instance, "make -C %p %o" expands to "make -C bar foo.vo"
+when module "foo" from directory "bar" is required.
+
+The default value is @code{""}.
+@end defopt
+
+
+@c TEXI DOCSTRING MAGIC: coq-compile-auto-save
+@defopt coq-compile-auto-save 
+Buffers to save before checking dependencies for compilation.@*
+There are two orthogonal choices: Firstly one can save all or only the coq
+buffers, where coq buffers means all buffers in coq mode except the current
+buffer. Secondly, emacs can ask about each such buffer or save all of them
+unconditionally.
+
+This makes four permitted values: @code{'ask-coq} to confirm saving all
+modified Coq buffers, @code{'ask-all} to confirm saving all modified
+buffers, @code{'save-coq} to save all modified Coq buffers without
+confirmation and @code{'save-all} to save all modified buffers without
+confirmation.
+
+The default value is @code{ask-coq}.
+@end defopt
+
+
+The following two options deal with the load path. Proof General
+divides the load path into the standard load path (which is
+hardwired in the tools and need not be set explicitly), the
+nonstandard load path (which must always be set explicitly), and
+the current directory (which must be set explicitly for
+@code{coqdep}). The option @code{coq-load-path} determines the
+nonstandard load path and @code{coq-load-path-include-current}
+determines whether the current directory is put into the load
+path of @code{coqdep}.
+
+@c TEXI DOCSTRING MAGIC: coq-load-path
+@defopt coq-load-path 
+Non-standard coq library load path.@*
+List of directories to be added to the LoadPath of coqdep, coqc
+and coqtop. Under normal circumstances this list does not need to
+contain "." for the current directory (see
+@samp{@code{coq-load-path-include-current}}) or the coq standard
+library.
+
+For coqdep and coqc these directories are passed via "-I"
+options over the command line. For interactive scripting an
+"Add LoadPath" command is used.
+
+The default value is @code{nil}.
+@end defopt
+
+
+@c TEXI DOCSTRING MAGIC: coq-load-path-include-current
+@defopt coq-load-path-include-current 
+If @samp{t} let coqdep search the current directory too.@*
+Should be @samp{t} for normal users. If @samp{t} pass "-I dir" to coqdep when
+processing files in directory "dir" in addition to any entries
+in @samp{@code{coq-load-path}}.
+
+The default value is @code{t}.
+@end defopt
+
+
+The following two options do only influence the behaviour if
+Proof General does dependency checking and compilation itself.
+These options determine whether Proof General should descend into
+other Coq libraries and into the Coq standard library. 
+
+@c TEXI DOCSTRING MAGIC: coq-compile-ignored-directories
+@defopt coq-compile-ignored-directories 
+Directories in which ProofGeneral should not compile modules.@*
+List of regular expressions for directories in which ProofGeneral
+should not compile modules. If a library file name matches one
+of the regular expressions in this list then ProofGeneral does
+neither compile this file nor check its dependencies for
+compilation. It makes sense to include non-standard coq library
+directories here if they are not changed and if they are so big
+that dependency checking takes noticeable time.
+
+The default value is @code{nil}.
+@end defopt
+
+
+@c TEXI DOCSTRING MAGIC: coq-compile-ignore-library-directory
+@defopt coq-compile-ignore-library-directory 
+If @samp{t} ProofGeneral does not compile modules from the coq library.@*
+Should be @samp{t} for normal coq users. If @samp{nil} library modules are
+compiled if their sources are newer.
+
+This option has currently no effect, because Proof General uses
+coqdep to translate qualified identifiers into library file names
+and coqdep does not output dependencies in the standard library.
+
+The default value is @code{t}.
+@end defopt
+
+
+The last three Emacs constants are internal parameters. They only
+need to be changed under very special, unforeseen circumstances.
+They can only be set in Emacs lisp code because they are no
+customizable user options.
+
+@c TEXI DOCSTRING MAGIC: coq-compile-substitution-list
+@defvar coq-compile-substitution-list 
+Substitutions for @samp{@code{coq-compile-command}}.@*
+Value must be a list of substitutions, where each substitution is
+a 2-element list. The first element of a substitution is the
+regexp to substitute, the second the replacement. The replacement
+is evaluated before passing it to @samp{@code{replace-regexp-in-string}}, so
+it might be a string, or one of the symbols @code{'physical-dir},
+@code{'module-object}, @code{'qualified-id} and @code{'requiring-file}, which are
+bound, respectively, to the the physical directory containing the
+source file, the Coq object file in @code{'physical-dir} that will be
+loaded, the qualified module identifier that occurs in the
+"Require" command, and the file that contains the
+"Require".
+@end defvar
+
+
+@c TEXI DOCSTRING MAGIC: coq-require-command-regexp
+@defvar coq-require-command-regexp 
+Regular expression matching Require commands in Coq.@*
+Should match "Require" with its import and export variants up to (but not
+including) the first character of the first required module. The required
+modules are matched separately with @samp{@code{coq-require-id-regexp}}
+@end defvar
+
+
+@c TEXI DOCSTRING MAGIC: coq-require-id-regexp
+@defvar coq-require-id-regexp 
+Regular expression matching one Coq module identifier.@*
+Should match precisely one complete module identifier and surrounding
+white space. The module identifier must be matched with group number 1.
+Note that the trailing dot in "Require A." is not part of the module
+identifier and should therefore not be matched by this regexp.
+@end defvar
+
+
+
+
+
 @node Editing multiple proofs
 @section Editing multiple proofs
 
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 9b0c876a..f5825516 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -931,7 +931,7 @@ 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
+    ((error quit)
      (proof-detach-queue)
      (signal (car err) (cdr err))))
   (proof-add-to-queue queueitems 'advancing))