Make coq-load-path accept either strings (which are passed "-I" options)
or conses of strings (which are passed as "-R" options).
Example:
> (setq coq-load-path '(("~/coq/math-classes/src" . "MathClasses")
"~/src/rippling"
("~/src/aac_tactics" . "AAC")))
> (coq-include-options nil)
("-R" "~/src/coq/math-classes/src" "MathClasses" "-I" "~/src/rippling" "-R"
"~/src/aac_tactics" . "AAC")
Signed-off-by: Tom Prince <[email protected]>
---
ProofGeneral-4.1RC4/coq/coq.el | 31 +++++++++++++++++++------------
1 files changed, 19 insertions(+), 12 deletions(-)
diff --git a/ProofGeneral-4.1RC4/coq/coq.el b/ProofGeneral-4.1RC4/coq/coq.el
index b218f08..34d0529 100644
--- a/ProofGeneral-4.1RC4/coq/coq.el
+++ b/ProofGeneral-4.1RC4/coq/coq.el
@@ -1331,9 +1331,12 @@ contain \".\" for the current directory (see
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."
- :type '(repeat string)
+or \"-R\" options over the command line. For interactive
+scripting an \"Add LoadPath\" command is used."
+ :type '(repeat (choice (string :tag "directory")
+ (cons :tag "recursive directory"
+ (string :tag "directory")
+ (string :tag "coq path"))))
:safe '(lambda (v) (every 'stringp v))
:group 'coq-auto-compile)
@@ -1482,15 +1485,19 @@ arguments with `nconc'.
FILE should be an absolute file name. It can be nil if
`coq-load-path-include-current' is nil."
- (let ((result nil))
- (when coq-load-path
- (setq result (list "-I" (expand-file-name (car coq-load-path))))
- (dolist (dir (cdr coq-load-path))
- (nconc result (list "-I" (expand-file-name dir)))))
- (if coq-load-path-include-current
- (setq result
- (cons "-I" (cons (file-name-directory file) result))))
- result))
+ (flet ((arg-from-option (arg)
+ (if (consp arg)
+ (list "-R" (expand-file-name (car arg)) (cdr
arg))
+ (list "-I" (expand-file-name arg)))))
+ (let ((result nil))
+ (when coq-load-path
+ (setq result (arg-from-option (car coq-load-path)))
+ (dolist (dir (cdr coq-load-path))
+ (nconc result (arg-from-option dir))))
+ (if coq-load-path-include-current
+ (setq result
+ (cons "-I" (cons (file-name-directory file) result))))
+ result)))
(defun coq-init-compile-response-buffer (command)
"Initialize the buffer for the compilation output.
--
1.7.6.1
_______________________________________________
ProofGeneral-devel mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
