Small refactoring of coqxxx args detection.

Need some more refactoring actually: Some code from coq-compile-common
became necessary to coq/pg globally. We shoudl refelct this by moving
these parts somewhere else.

3 files changed, 44 insertions, 42 deletions

diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index 48d62cfb..2e8919f1 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -504,8 +504,7 @@ options they are translated."
   "Build the list of include options for coqc, coqdep and coqtop.
 The options list includes all entries from argument COQ-LOAD-PATH
 \(which should be `coq-load-path' of the buffer that invoked the
-compilation)
-prefixed with suitable options and, if
+compilation) prefixed with suitable options and (for coq<8.5), if
 `coq-load-path-include-current' is enabled, the directory base of
 FILE. The resulting list is fresh for every call, callers can
 append more arguments with `nconc'.
@@ -523,35 +522,35 @@ FILE should be an absolute file name. It can be nil if
         (setq result
               (if coq-pre-v85
 		  (cons "-I" (cons (file-name-directory file) result))
-		(cons "-Q" (cons (file-name-directory file) (cons "" result))))))
+		;; from coq-8.5 beta3 cpqdep does not needthis anymore
+		;; and actually it can clash with -Q . foo written in
+		;; _CoqProject
+		;; (cons "-Q" (cons (file-name-directory file) (cons "" result)))
+		result)))
     result))
 
-(defun coq-coqc-prog-args (&optional src-file coq-load-path-opt)
-  ;; coqtop always adds the current directory to the LoadPath, so
-  ;; don't include it in the -Q options. This is not true for coqdep
-  ;; until late 8.5 betas.
-  (let* ((coq-loadpath (or coq-load-path-opt coq-load-path))
-	 (coq-load-path-include-current nil)
-	 )
-    ;; delete is safe here since coq-include-optionsbuilds a fresh list
-    ;; TODO: replace remove by delete?
-    (remove "-emacs"
-	    (remove "-emacs-U"
-		    (append coq-prog-args (coq-include-options src-file coq-loadpath))))))
-
-;; FIXME: this function seems to have a strange influence on pg. Is it
-;; interfering with defpgcustom prog-args in pg-custom.el?
-(defun coq-prog-args (&optional src-file loadpath)
-  ;; coqtop always adds the current directory to the LoadPath, so don't
-  ;; include it in the -Q options. This is not true for coqdep.
-  (let ((loadpath (or loadpath coq-load-path))
-	(coq-load-path-include-current nil))
-    (append coq-prog-args (coq-include-options src-file loadpath))))
+
+(defun coq-coqdep-prog-args (&optional src-file loadpath)
+  (let ((loadpath (or loadpath coq-load-path)))
+    (coq-include-options src-file loadpath)))
 
 (defun coq-coqc-prog-args (&optional src-file loadpath)
   ;; coqtop always adds the current directory to the LoadPath, so don't
+  ;; include it in the -Q options.
+  (let ((coqdep-args
+	 (let ((coq-load-path-include-current nil)) ; obsolete >=8.5beta3
+	   (append coq-prog-args (coq-coqdep-prog-args src-file loadpath)))))
+    (remove "-emacs" (remove "-emacs-U" coqdep-args))))
+
+(defun coq-coqtop-prog-args (&optional src-file loadpath)
+  ;; coqtop always adds the current directory to the LoadPath, so don't
   ;; include it in the -Q options. This is not true for coqdep.
-  (remove "-emacs" (remove "-emacs-U" (coq-prog-args src-file loadpath))))
+  (cons "-emacs" (coq-coqc-prog-args src-file loadpath)))
+
+;; FIXME: we seem to need this function with this exact name,
+;; otherwise coqtop command is not generated with the good load-path
+;; (??). Is it interfering with defpgcustom's in pg-custom.el?
+(defun coq-prog-args () (coq-coqtop-prog-args))
 
 
 
diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index f469b4df..fac1ff35 100644
--- a/coq/coq-par-compile.el
+++ b/coq/coq-par-compile.el
@@ -452,13 +452,23 @@ belonging to the circle."
 
 ;;; map coq module names to files, using synchronously running coqdep 
 
-(defun coq-par-coq-arguments (lib-src-file coq-load-path)
+(defun coq-par-coqdep-arguments (lib-src-file coq-load-path)
   "Compute the command line arguments for invoking coqdep on LIB-SRC-FILE.
 Argument COQ-LOAD-PATH must be `coq-load-path' from the buffer
 that triggered the compilation, in order to provide correct
 load-path options to coqdep."
-  (nconc (coq-include-options lib-src-file coq-load-path)
-	 (list lib-src-file)))
+  (nconc ;(coq-include-options lib-src-file coq-load-path)
+   (coq-coqdep-prog-args lib-src-file coq-load-path)
+   (list lib-src-file)))
+
+(defun coq-par-coqc-arguments (lib-src-file coq-load-path)
+  "Compute the command line arguments for invoking coqdep on LIB-SRC-FILE.
+Argument COQ-LOAD-PATH must be `coq-load-path' from the buffer
+that triggered the compilation, in order to provide correct
+load-path options to coqdep."
+  (nconc ;(coq-include-options lib-src-file coq-load-path)
+   (coq-coqc-prog-args lib-src-file coq-load-path)
+   (list lib-src-file)))
 
 (defun coq-par-analyse-coq-dep-exit (status output command)
   "Analyse output OUTPUT of coqdep command COMMAND with exit status STATUS.
@@ -504,7 +514,7 @@ dependencies are absolute too and the simplified treatment of
 `coq-load-path-include-current' in `coq-include-options' won't
 break."
   (let* ((coqdep-arguments
-	  (coq-par-coq-arguments lib-src-file coq-load-path))
+	  (coq-par-coqdep-arguments lib-src-file coq-load-path))
 	 (this-command (cons coq-dependency-analyzer coqdep-arguments))
 	 (full-command (if command-intro
 			   (cons command-intro this-command)
@@ -978,7 +988,7 @@ locked, registered in the 'ancestor-files property of JOB and in
 	(puthash true-src 'locked coq-par-ancestor-files)))
     (coq-par-start-process
      coq-dependency-analyzer
-     (coq-par-coq-arguments (get job 'src-file) (get job 'load-path))
+     (coq-par-coqdep-arguments (get job 'src-file) (get job 'load-path))
      'coq-par-process-coqdep-result
      job)))
 
@@ -994,7 +1004,7 @@ coqdep or coqc are started for it."
       (message "Recompile %s" (get job 'src-file))
       (coq-par-start-process
        coq-compiler
-       (coq-par-coq-arguments (get job 'src-file) (get job 'load-path))
+       (coq-par-coqc-arguments (get job 'src-file) (get job 'load-path))
        'coq-par-coqc-continuation
        job)))))
 
diff --git a/coq/coq.el b/coq/coq.el
index 743d49a7..a08ca3f4 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -71,6 +71,7 @@
 ;;; Code:
 ;; debugging functions
 ;; (defun proofstack () (coq-get-span-proofstack (span-at (point) 'type)))
+(defvar coq-debug nil)
 ;; End debugging
 
 (defcustom coq-prog-name
@@ -104,16 +105,6 @@ and 8.5 (-Q foo bar replace -I foo)."
   :type 'boolean
   :group 'coq)
 
-(defun coq-build-prog-args ()
-  "Adjusts default `coq-prog-args'.  May be overridden by file variables."
-  (delete "-emacs" coq-prog-args)
-  (add-to-list 'coq-prog-args "-emacs-U")
-  (if coq-translate-to-v8 
-      (add-to-list 'coq-prog-args "-translate")))
-
-(unless noninteractive   ;; compiling
-  (coq-build-prog-args))
-
 (defcustom coq-use-makefile nil
   "Whether to look for a Makefile to attempt to guess the command line.
 Set to t if you want this feature."
@@ -1493,6 +1484,9 @@ allows to call coqtop from a subdirectory of the project."
          (if (or avoidpath avoidargs)
              (concat "\n(" msg " overridden by dir/file local values)")
            "")))
+      (when coq-debug
+        (message "coq-prog-args: %S" coq-prog-args)
+        (message "coq-load-path: %S" coq-load-path))
       (unless no-kill (kill-buffer projectbuffer)))))
 
 
@@ -1560,7 +1554,6 @@ Warning:
   ;; again is useless. Let us do nothing.
   ;;(setq coq-load-path nil)
   ;;(setq coq-prog-args nil)
-  ;;(coq-build-prog-args)
   )