- simple backward compatible change to invoke a function to

  compute the command line arguments for a proof assistant

2 files changed, 20 insertions, 6 deletions

diff --git a/coq/coq.el b/coq/coq.el
index 0e527e87..23711346 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1239,6 +1239,14 @@ The first integer contains the upper 16 bits and the second the lower
         t)
     nil))
 
+;; Compute command line for starting coqtop
+
+(defun coq-prog-args ()
+  ;; coqtop always adds the current directory to the LoadPath, so don't
+  ;; include it in the -I options.
+  (let ((coq-load-path-include-current nil))
+    (append coq-prog-args (coq-include-options nil))))
+
 ;; handle Require commands when queue is extended
 
 (defun coq-recompile-ignore-file (lib-obj-file)
@@ -1273,7 +1281,8 @@ 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'.
 
-FILE should be an absolute file name."
+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))))
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index a09ddd78..9b0c876a 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -234,11 +234,16 @@ process command."
 
       ;; Starting the inferior process (asynchronous)
       (let* ((prog-name-list1
-	      (if (proof-ass prog-args)
-		 ;; If argument list supplied in <PA>-prog-args, use that.
-		  (cons proof-prog-name (proof-ass prog-args))
-		;; Otherwise, cut prog name on spaces
-		(split-string proof-prog-name)))
+	      (if (functionp (proof-ass-sym prog-args))
+		  ;; complex assistants define <PA>-prog-args as function
+		  ;; that computes the argument list.
+		  (cons proof-prog-name (funcall  (proof-ass-sym prog-args)))
+		(if (proof-ass prog-args)
+		    ;; Intermediate complex assistants set the value
+		    ;; of <PA>-prog-args to the argument list.
+		    (cons proof-prog-name (proof-ass prog-args))
+		  ;; Trivial assistants simply set proof-prog-name
+		  (split-string proof-prog-name))))
 	     (prog-name-list
 	      ;; Splice in proof-rsh-command if it's non-nil
 	      (if (and proof-rsh-command