Should fix #49 and #55 (compilation of From .. Require).

3 files changed, 22 insertions, 18 deletions

diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index 415f65ee..8ce4b0c2 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -300,12 +300,6 @@ the latter condition into an error, then set this variable to
   :safe 'stringp
   :group 'coq-auto-compile)
 
-(defconst coq-require-command-regexp
-  "^Require[ \t\n]+\\(Import\\|Export\\)?[ \t\n]*"
-  "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 `coq-require-id-regexp'")
 
 (defconst coq-require-id-regexp
   "[ \t\n]*\\([A-Za-z0-9_']+\\(\\.[A-Za-z0-9_']+\\)*\\)[ \t\n]*"
@@ -315,6 +309,13 @@ 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.")
 
+(defconst coq-require-command-regexp
+  "\\(?:^From[ \t\n]+\\(?1:[A-Za-z0-9_']+\\(?:\\.[A-Za-z0-9_']+\\)*\\)[ \t\n]*\\)?\\(?2:Require[ \t\n]+\\(?:Import\\|Export\\)?\\)[ \t\n]*"
+  "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 `coq-require-id-regexp'")
+
 (defvar coq-compile-history nil
   "History of external Coq compilation commands.")
 
diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index 5c37c382..840a1598 100644
--- a/coq/coq-par-compile.el
+++ b/coq/coq-par-compile.el
@@ -534,7 +534,7 @@ break."
     ;;              coqdep-status lib-src-file coqdep-output))
     (coq-par-analyse-coq-dep-exit coqdep-status coqdep-output full-command)))
 
-(defun coq-par-map-module-id-to-obj-file (module-id coq-load-path)
+(defun coq-par-map-module-id-to-obj-file (module-id coq-load-path &optional from)
   "Map MODULE-ID to the appropriate coq object file.
 The mapping depends of course on `coq-load-path'. The current
 implementation invokes coqdep with a one-line require command.
@@ -553,7 +553,8 @@ function returns () if MODULE-ID comes from the standard library."
            coq-load-path))
         (coq-load-path-include-current nil)
         (temp-require-file (make-temp-file "ProofGeneral-coq" nil ".v"))
-        (coq-string (concat "Require " module-id "."))
+        (coq-string (concat (if from (concat "From " from " ") "")
+                            "Require " module-id "."))
         result)
     (unwind-protect
         (progn
@@ -1184,7 +1185,7 @@ PROCESS."
 
 ;;; handle Require commands when queue is extended
 
-(defun coq-par-handle-module (module-id span)
+(defun coq-par-handle-module (module-id span &optional from)
   "Handle compilation of module MODULE-ID.
 This function translates MODULE-ID to a file name. If compilation
 for this file is not ignored, a new top-level compilation job is
@@ -1195,7 +1196,7 @@ This function must be evaluated with the buffer that triggered
 the compilation as current, otherwise a wrong `coq-load-path'
 might be used."
   (let ((module-obj-file
-	 (coq-par-map-module-id-to-obj-file module-id coq-load-path))
+	 (coq-par-map-module-id-to-obj-file module-id coq-load-path from))
 	module-job)
     (if coq-debug-auto-compilation
         (message "check compilation for module %s from object file %s"
@@ -1231,11 +1232,12 @@ there is no last compilation job."
   (let* ((item (car require-items))
 	 (string (mapconcat 'identity (nth 1 item) " "))
 	 (span (car item))
-	 start)
+         prefix start)
     ;; We know there is a require in string. But we have to match it
     ;; again in order to get the end position.
     (string-match coq-require-command-regexp string)
     (setq start (match-end 0))
+    (setq prefix (match-string 1 string))
     (span-add-delete-action
      span
      `(lambda ()
@@ -1243,7 +1245,7 @@ there is no last compilation job."
     ;; add a compilation job for all required modules
     (while (string-match coq-require-id-regexp string start)
       (setq start (match-end 0))
-      (coq-par-handle-module (match-string 1 string) span))
+      (coq-par-handle-module (match-string 1 string) span prefix))
     ;; add the asserted items to the last compilation job
     (if coq-last-compilation-job
 	(progn
diff --git a/coq/coq-seq-compile.el b/coq/coq-seq-compile.el
index e00a2793..da85ad9f 100644
--- a/coq/coq-seq-compile.el
+++ b/coq/coq-seq-compile.el
@@ -284,7 +284,7 @@ therefore the customizations for `compile' do not apply."
        span
        (coq-library-src-of-obj-file absolute-module-obj-file)))))
 
-(defun coq-seq-map-module-id-to-obj-file (module-id span)
+(defun coq-seq-map-module-id-to-obj-file (module-id span &optional from)
   "Map MODULE-ID to the appropriate coq object file.
 The mapping depends of course on `coq-load-path'. The current
 implementation invokes coqdep with a one-line require command.
@@ -301,7 +301,7 @@ function returns () if MODULE-ID comes from the standard library."
            coq-load-path))
         (coq-load-path-include-current nil)
         (temp-require-file (make-temp-file "ProofGeneral-coq" nil ".v"))
-        (coq-string (concat "Require " module-id "."))
+        (coq-string (concat (if from (concat "From " from " ") "") "Require " module-id "."))
         result)
     (unwind-protect
         (progn
@@ -337,7 +337,7 @@ function returns () if MODULE-ID comes from the standard library."
             "Internal error in coq-seq-map-module-id-to-obj-file")
     (car-safe result)))
 
-(defun coq-seq-check-module (coq-object-local-hash-symbol span module-id)
+(defun coq-seq-check-module (coq-object-local-hash-symbol span module-id &optional from)
   "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
@@ -354,7 +354,7 @@ the coq-obj-hash, which is used during internal
 compilation (see `coq-seq-make-lib-up-to-date'). This way one hash
 will be used for all \"Require\" commands added at once to the
 queue."
-  (let ((module-obj-file (coq-seq-map-module-id-to-obj-file module-id span)))
+  (let ((module-obj-file (coq-seq-map-module-id-to-obj-file module-id span from)))
     ;; coq-seq-map-module-id-to-obj-file currently returns () for
     ;; standard library modules!
     (when module-obj-file
@@ -382,7 +382,8 @@ compilation (if necessary) of the dependencies."
             (when (and string
                        (string-match coq-require-command-regexp string))
               (let ((span (car item))
-                    (start (match-end 0)))
+                    (start (match-end 0))
+                    (prefix (match-string 1 string)))
                 (span-add-delete-action
                  span
                  `(lambda ()
@@ -392,7 +393,7 @@ compilation (if necessary) of the dependencies."
                 (while (string-match coq-require-id-regexp string start)
                   (setq start (match-end 0))
                   (coq-seq-check-module 'coq-object-hash-symbol span
-                                    (match-string 1 string))))))))))
+                                    (match-string 1 string) prefix)))))))))
 
 
 (provide 'coq-seq-compile)