cpitclaudel/company-coq

`M-.` failure

vzaliva opened this issue · 6 comments

vzaliva commented

Pressing M-. on definition fails with error "company-coq--get-comment-region: Symbol’s function definition is void: coq-find-comment-start"

Isweet commented

I'm also getting this error.

OSX Version 10.14.6
Emacs Version 26.2
Coq Version 8.9.1
Proof General Version 20190821.848
Company-Coq Version 20190425.1851

vzaliva commented

It started happening again

cpitclaudel commented

OK, I'll take a look at getting a better fix this week-end

vzaliva commented

thanks! It is really annoyng bug as it is very common functionality used often.

vzaliva commented

I did some additional digging, and functions coq-find-comment-start and coq-find-comment-end are commented out in current MELPA version (20191007.1041) of proof general's coq-indent.el ( https://github.com/ProofGeneral/PG/blob/master/coq/coq-indent.el#L284 ).

vzaliva commented

Currently, this works, fixed by ProofGeneral/PG#444
However, they had a suggestion:

Probably a better option is to fix company-coq so it uses
syntax-ppss and forward-comment instead. E.g.

    (let ((ppss (syntax-ppss))) (when (nth 4 ppss) (nth 8 ppss))))

will return the position of the beginning of the comment if you're
inside a comment or nil otherwise. And (forward-comment 1) will jump
from the beginning of a comment to its end.

I leave this issue open for now. If you do not plan to implement this suggestion and happy with current mechanism, feel free to close it.