search

cpitclaudel / company-coq

A Coq IDE build on top of Proof General's Coq mode
GNU General Public License v3.0
352 stars 29 forks source link

Feature request: don't disable multiword completions after space #49

Open JasonGross opened 8 years ago

JasonGross commented 8 years ago

If I type Set P, my completions are all gone. It'd be nice to still have completions for things like Set Printing Implicit.

cpitclaudel commented 8 years ago

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.

JasonGross commented 8 years ago

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?

cpitclaudel commented 8 years ago

No, completion isn't stateful: after every character typed, backends get queried for a prefix, and subsequently for candidates given that prefix.

JasonGross commented 8 years ago

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?

cpitclaudel commented 8 years ago

I thought about this; there are two issues:

  1. 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.
  2. It would introduce an inconsistency: Set Pr completes, but not Set 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?

JasonGross commented 8 years ago
  1. 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.
  2. 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.
cpitclaudel commented 8 years ago

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 :/

cpitclaudel commented 8 years ago

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?

cpitclaudel commented 8 years ago

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.

JasonGross commented 8 years ago

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?

cpitclaudel commented 8 years ago

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

JasonGross commented 8 years ago

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

cpitclaudel commented 8 years ago

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?

JasonGross commented 8 years ago

I was not aware. Cool!

jstolarek commented 8 years ago

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?

cpitclaudel commented 8 years ago

@jstolarek Note that this already works, actually: typing SetPImpl does suggest Set Printing Implicit :)

jstolarek commented 8 years ago

Ha! Somehow it did not cross my mind to actually try it out :-) Need to change my muscle-memory to Java style.