FIX #422.

the output of coqtop-help is now stored in a variable like coq's version.

1 files changed, 44 insertions, 21 deletions

diff --git a/coq/coq-system.el b/coq/coq-system.el
index 839553e7..8febc1c8 100644
--- a/coq/coq-system.el
+++ b/coq/coq-system.el
@@ -70,6 +70,10 @@ variable should contain nil or a version string."
 (defvar coq-autodetected-version nil
   "Version of Coq, as autodetected by `coq-autodetect-version'.")
 
+(defvar coq-autodetected-help nil
+  "Options of Coq, as autodetected by `coq-autodetect-options'.
+This variable contains the output of \"coqtop -help\"")
+
 ;;; error symbols
 
 ;; coq-unclassifiable-version
@@ -102,33 +106,46 @@ If it doesn't look right, try `coq-autodetect-version'."
         (message "Using Coq v%s" coq-autodetected-version)
       (message "Coq version unknown at this time. Use `coq-autodetect-version' to autodetect."))))
 
+(defun coq-callcoq (option &optional expectedretv)
+  "Call coqtop with the given OPTION and return the output.
+The given option should make coqtop return immediately.
+Optionally check the return code and return nil if the check
+fails.
+This function supports calling coqtop via tramp."
+  (let* ((default-directory
+           (if (file-accessible-directory-p default-directory)
+               default-directory
+             "/"))
+         (coq-command (shell-quote-argument (or coq-prog-name "coqtop")))) 
+    (with-temp-buffer
+      ;; Use `shell-command' via `find-file-name-handler' instead of
+      ;; `process-line': when the buffer is running TRAMP, PG uses
+      ;; `start-file-process', loading the binary from the remote server.
+      (let* ((shell-command-str (format "%s %s" coq-command (or option "")))
+             (fh (find-file-name-handler default-directory 'shell-command))
+             (retv (if fh (funcall fh 'shell-command shell-command-str (current-buffer))
+                     (shell-command shell-command-str (current-buffer)))))
+        (if (or (not expectedretv) (equal retv expectedretv))
+            (buffer-string))))))
+
 (defun coq-autodetect-version (&optional interactive-p)
   "Detect and record the version of Coq currently in use.
 Interactively (with INTERACTIVE-P), show that number."
   (interactive '(t))
   (setq coq-autodetected-version nil)
-  (with-temp-buffer
-    ;; Use `shell-command' via `find-file-name-handler' instead of
-    ;; `process-line': when the buffer is running TRAMP, PG uses
-    ;; `start-file-process', loading the binary from the remote server.
-    (let* ((default-directory
-	     (if (file-accessible-directory-p default-directory)
-		 default-directory
-	       "/"))
-	   (coq-command (shell-quote-argument (or coq-prog-name "coqtop")))
-           (shell-command-str (format "%s -v" coq-command))
-           (fh (find-file-name-handler default-directory 'shell-command))
-           (retv (if fh (funcall fh 'shell-command shell-command-str (current-buffer))
-                   (shell-command shell-command-str (current-buffer)))))
-      (when (equal 0 retv)
-        ;; Fail silently (in that case we'll just assume Coq 8.5)
-        (goto-char (point-min))
-        (when (re-search-forward "version \\([^ ]+\\)" nil t)
-          (setq coq-autodetected-version (match-string 1))))))
-  (when interactive-p
-    (coq-show-version))
+  (let* ((str (coq-callcoq "-v" 0))
+         (mtch (and str (string-match "version \\([^ ]+\\)" str))))
+    (when mtch
+      (setq coq-autodetected-version (match-string 1 str))))
+  (when interactive-p (coq-show-version))
   coq-autodetected-version)
 
+(defun coq-autodetect-help (&optional interactive-p)
+  "Record the output of coqotp -help in `coq-autodetected-help'."
+  (interactive '(t))
+  (setq coq-autodetected-help (coq-callcoq "-help")))
+
+
 (defun coq--version< (v1 v2)
   "Compare Coq versions V1 and V2."
   ;; -snapshot is only supported by Emacs 24.5, not 24.3
@@ -180,6 +197,11 @@ Return nil if the version cannot be detected."
 	 (signal 'coq-unclassifiable-version  coq-version-to-use))
 	(t (signal (car err) (cdr err))))))))
 
+(defun coq--supports-topfile ()
+  "Return t if \"-topfile\" appears in coqtop options"
+  (string-match "-topfile" coq-autodetected-help)
+)
+
 (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, but note that it is deprecated."
@@ -410,13 +432,14 @@ LOADPATH, CURRENT-DIRECTORY, PRE-V85: see `coq-include-options'."
   "Build a list of options for coqc.
 LOADPATH, CURRENT-DIRECTORY, PRE-V85: see `coq-coqc-prog-args'."
   (append
-   (if (coq--post-v810) (cons "-topfile" (cons buffer-file-name nil)) "")
+   (if (coq--supports-topfile) (cons "-topfile" (cons buffer-file-name nil)) "")
    (cons "-emacs" (coq-coqc-prog-args loadpath current-directory pre-v85))))
 
 (defun coq-prog-args ()
   "Recompute `coq-load-path' before calling `coq-coqtop-prog-args'."
   (coq-load-project-file)
   (coq-autodetect-version)
+  (coq-autodetect-help)
   (coq-coqtop-prog-args coq-load-path))
 
 (defcustom coq-use-project-file t