Completion for End should give correct section

[tchajed]

I thought company-coq already had a feature for this but couldn't find it.

It would be nice if company-coq completed the End command with the section name computed by Proof General's coq-end-Section. This would best be done by factoring out coq-last-opened-section (since the method currently inserts the computed section name).

As I mentioned in ProofGeneral/PG#100, it would also be nice if these commands worked for modules and module types in the same way, since all of these blocks are fairly similar.

[cpitclaudel]

I think it does, actually :) Is it broken? I have a queue of patches that I haven't pushed, because deadlines and Master's thesis, so I could have fixed it locally a few weeks ago.

[cpitclaudel]

That feature could use some love, though. Right now it only kicks in after a few characters, which is arguably not too useful.

[tchajed]

Yes - it seems to work if you type the first 3 characters correctly. At first I thought it was completing all open sections/modules but it actually seems to pick the closest one. If course I'd rather not have to get any characters right, since I typically want this when I don't remember what the name is and it's off-screen.

At least from the company-backends documentation it looks like a company-backend should be able to express this, if not directly from completing End then completion right after it. I'll see if I can piece together how to do it at some point.

With this working I won't care much about ProofGeneral/PG#100, at least for my own setup - autocompletion is the best API I can imagine here.

[cpitclaudel]

Yeah, it shouldn't be too hard. We just need to mark that backend as ignoring the user-customized prefix length, since "End " serves as an implicit prefix.

[tchajed]

Cool, I'll figure out how to do that.

[cpitclaudel]

Neat. You'll want to look at company-coq-candidates-block-end, and to tweak company-coq-line-is-block-end-p as well as company-coq-block-end-regexp. The prefix length part might be a bit tricky due to backend grouping in company-coq-master-backend, so maybe getting it to work with just company-coq-block-end-backend is a good start :)