coq-find-comment-start, coq-find-comment-end commented out

[vzaliva]

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 ).

These functions are used by M-. functionality of company-coq which is now broken: cpitclaudel/company-coq#225

Is there is a reason for commenting them out and perhaps they could be restored?

[erikmd]

@vzaliva thanks for the report!

The code you mention has been commented-out by @monnier with this refactoring commit:
fb3b75d - IIUC (according to the commit message), this code has been removed as it wasn't used elsewhere in PG (while company-coq does depend on it as you point out !-) so I guess this removal can/should be reverted.

I've no time this week but if you can prepare a PR that reverts these coq-indent.el removals, I'd be happy to integrate it.

[monnier]

The code you mention has been commented-out by @monnier with this refactoring commit: fb3b75d - IIUC (according to the commit message), this code has been removed as it wasn't used elsewhere in PG (while company-coq does depend on it as you point out !-) so I guess this removal can/should be reverted.

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. Stefan

[vzaliva]

Does it work with nested comments? The previous function description states "If inside nested comments, go to the start of the outer most comment."

[vzaliva]

It is up to @cpitclaudel to change company-coq. I am afraid I am no up to this task. I am just a user trying to fix the tool I use every day. I will be happy to submit PR undoing removal of these functions in PG. This is easy enough :)

[vzaliva]

Verified and the issue is fixed with the recent MELPA update. Thanks!

[erikmd]

Thanks @vzaliva !