diff options
| -rw-r--r-- | coq/coq-syntax.el | 1 | ||||
| -rw-r--r-- | coq/coq-system.el | 17 | ||||
| -rw-r--r-- | coq/coq.el | 5 |
3 files changed, 18 insertions, 5 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 91e6b9d3..a349ec55 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1367,6 +1367,7 @@ It is used: ;; constituent (better behavior for thing-at and maybe font-lock too, ;; for indentation we use ad hoc smie lexers). (defmacro coq-with-altered-syntax-table (&rest code) + (declare (debug t)) (let ((res (make-symbol "res"))) `(unwind-protect (progn (modify-syntax-entry ?\. "_") diff --git a/coq/coq-system.el b/coq/coq-system.el index 2a803f36..8e0f9034 100644 --- a/coq/coq-system.el +++ b/coq/coq-system.el @@ -99,9 +99,20 @@ If it doesn't look right, try `coq-autodetect-version'." Interactively (with INTERACTIVE-P), show that number." (interactive '(t)) (setq coq-autodetected-version nil) - (let ((version-string (car (process-lines (or coq-prog-name "coqtop") "-v")))) - (when (and version-string (string-match "version \\([^ ]+\\)" version-string)) - (setq coq-autodetected-version (match-string 1 version-string)))) + (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* ((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)) coq-autodetected-version) @@ -876,8 +876,9 @@ Support dot.notation.of.modules." (defun coq-id-or-notation-at-point () - (or (coq-id-at-point) (concat "\"" (coq-notation-at-position (point)) "\""))) - + (or (coq-id-at-point) + (let ((notation (coq-notation-at-position (point)))) + (if notation (concat "\"" notation "\"") "")))) (defcustom coq-remap-mouse-1 nil "Wether coq mode should remap mouse button 1 to coq queries. |