Skip to content

Commit

Permalink
strip _build/default when locating files
Browse files Browse the repository at this point in the history
  • Loading branch information
MackieLoeffel committed Jan 24, 2023
1 parent 5affe7a commit 6b506e3
Showing 1 changed file with 11 additions and 6 deletions.
17 changes: 11 additions & 6 deletions company-coq.el
Original file line number Diff line number Diff line change
Expand Up @@ -2180,12 +2180,17 @@ to a non-existent file (for an example of such a case, try
(file-name-nondirectory (buffer-file-name proof-script-buffer))))))
proof-script-buffer
(let* ((lib-name (concat lib-path mod-name))
(output (company-coq-ask-prover-swallow-errors (format company-coq-locate-lib-cmd lib-name))))
(or (and output (save-match-data
(when (and (string-match company-coq-locate-lib-output-format output)
(string-match-p company-coq-compiled-regexp (match-string-no-properties 3 output)))
(concat (match-string-no-properties 2 output) ".v"))))
(and fallback-spec (expand-file-name (concat mod-name ".v") (cdr fallback-spec)))))))
(output (company-coq-ask-prover-swallow-errors (format company-coq-locate-lib-cmd lib-name)))
(path (or (and output (save-match-data
(when (and (string-match company-coq-locate-lib-output-format output)
(string-match-p company-coq-compiled-regexp (match-string-no-properties 3 output)))
(concat (match-string-no-properties 2 output) ".v"))))
(and fallback-spec (expand-file-name (concat mod-name ".v") (cdr fallback-spec)))))
(stripped (replace-regexp-in-string "_build/default" "" path nil 'literal)))
(if (file-exists-p stripped)
stripped
path
))))

(defun company-coq--locate-name (name functions)
"Find location of NAME using FUNCTIONS.
Expand Down

0 comments on commit 6b506e3

Please sign in to comment.