company-coq
company-coq copied to clipboard
cpitclaudel
Feature request: don't disable multiword completions after space
If I type Set P, my completions are all gone. It'd be nice to still have completions for things like Set Printing Implicit.
Agreed, but very hard to do; scanning backward to know where completions should start is hard.
Would this work instead? Don't type Set P for Set Printing Implicit; use SPI.
I think that would take time for my fingers to learn; I tend to acquire these by typing less and less of the keyword as I go along. Is completion stateful? Could you simply remember the point where the current completion started?
No, completion isn't stateful: after every character typed, backends get queried for a prefix, and subsequently for candidates given that prefix.
Maybe for the options (the things that come after Set), you can offer completions for just those things? This seems like an ugly hack, but might have the behavior I want?
I thought about this; there are two issues:
- Normally completion only starts after you type three characters (company only asks company-coq for candidates after the prefix is 3 characters or more); but here the prefix is empty. Lowering the start threshold would has a significant performance cost, due to the number of completions.
- It would introduce an inconsistency:
Set Prcompletes, but notSet Printing Impl? Of course I could generalize the trick, but it becomes a bit of a mess.
I'll keep this open; maybe we're missing a great idea here?
- Won't work for me. There are already too many completions for just
Set, I want to be able to narrow it down more, first. - This is why it's a kludge. But I wouldn't mind too much, because usually I notice the completions by the time I get to
Set Pr.
By 1. I meant that 1. was one of the reason why this was tricky to implement: company doesn't ask company-coq for candidates after you type Set. Even getting it to do that would be a hack :/
Here's a different form of retraining, which might be slightly nicer on the muscle memory: can you omit the spaces? That is, can you use SetPrinting instead of Set Printing?
Thinking more about this, there's another possibility: I could change the prefix function so that "Set " is considered a valid prefix. That would mean that after typing "Set Pr", you would continue getting candidates such as "Set Printing" etc, but you wouldn't get "Prop", for example.
That's a very easy change; I could push it to a branch if you want to try it out.
There are very few cases that I'd want Set Pr to give me Prop. If I type Goal Pro, I should still get Prop. Can you instead make it an option that's disabled by default, on master, so that I can try it from melpa?
Sure! It's done. You can turn the new option on using (setq company-coq--use-special-set-unset-test-regexp t) and off using (setq company-coq--use-special-set-unset-test-regexp nil).
Thanks! This is working well! Can you also do the same thing for Set Printing and Unset Printing? There are so many options there that the completion is only helpful if I can use it after the printing. (Though I guess you'll suggest that I use SPUn?)
Yeah, this is getting really hackish, isn't it?
By the way, are you aware of C-s and C-M-s in company's popup?
Would this work instead? Don't type Set P for Set Printing Implicit; use SPI.
This would work for me - I used to program in Java, where this is kind of natural way of using autocompletion. Actually, in editors like Eclipse I can autocomplete anything written in a camel case by typing first letters of the words. So in the above example SetPImpl should also allow to autocomplete. In fact, emacs does the same thing but instead of paying attention to capital letters it uses dashes. If I type M-x pro-e-t-tog and press TAB this gets completed as proof-electric-terminator-toggle. So the machinery seems to be there. Perhaps there is a way to piggyback on it?
@jstolarek Note that this already works, actually: typing SetPImpl does suggest Set Printing Implicit :)
Ha! Somehow it did not cross my mind to actually try it out :-) Need to change my muscle-memory to Java style.