coq_nvim

coq_nvim copied to clipboard

I'm one of those people who likes the way completion works in vanilla vim (because it saves me one keystroke, and I have muscle memory for it). It usually works like this: I see the suggestion, I press ctrl+n until I arrive at the one I want, and then I move on, without needing to press Enter. This mostly works with coq_nvim, but there is no visual feedback that the suggestion has been inserted. Only when I type another character (like space) does it become visible that the suggestion has been inserted.

Is this something you could support?

My settings at the moment are

vim.opt.completeopt = {'menuone', 'noselect'}
vim.opt.shortmess:append({ c = true })  -- aka `shortmess+=c`

vim.g.coq_settings = {
  ["keymap.recommended"] = false,
}

You can see in this image how I have already selected items but in the buffer there is still only ite.

When I press space, the text is inserted:

sorry I dont really know exactly what you mean, do you mean that when you do <c-p> and <c-n>, it shows you like a preview of what would be inserted?

coq.nvim doesn't work that way because it has fuzzy logic and doesn't just change whatever is after the symbol, it might also change the symbol itself too.

By symbol, I mostly mean the word under cursor, but can also be non-words too, depending on the context.

I tried getting that preview thing to work that way before, but it didnt really work well, since you need to know where exactly to place the popup menu, or else vim will start overwriting the wrong information.

It's not super hard to compute, but does have weird implications, because you would be placing the menu essentially on the leftmost position of the computed position of any of the suggestions, and that could result in really weird experiences like having a suggestion popup as you type left to right, but the presence of the suggestion actually takes the menu more left.

Hm, no, that's not what I mean. I think I just don't want to set noinsert in completeopt. But it is hard coded here: https://github.com/ms-jpq/coq_nvim/blob/coq/coq/server/registrants/options.py#L65

EDIT: Basically, I have the opposite problem of this person: https://vi.stackexchange.com/questions/19971/ctrl-n-should-not-insert-text . I want ctrl+n to insert the text (which it does in normal vim).

As an investigation, I modified coq/server/registrants/options.py to remove noinsert from there, but it still doesn't work as expected. On the other hand, removing noselect had an effect, so I'm pretty sure I edited the correct place. I think this means that something else is preventing the selected suggestion from being inserted. Maybe it's something important; I don't know.

This also causes another problem: if you first select a match using <C-P> or <C-N>, then select another match using <PageUp> or <PageDown>, then press <Space>, the match selected using <C-P> or <C-N> is inserted instead of the match selected using <PageUp> or <PageDown>.

Also I think this is what prevents the selected suggestion from being inserted:

https://github.com/ms-jpq/coq_nvim/blob/fc6fa8a3cf91858dcd81e9771f0a6d69284be81c/coq/server/trans.py#L121

And fuzzy completion requires this.

Hm, no, that's not what I mean. I think I just don't want to set noinsert in completeopt. But it is hard coded here: https://github.com/ms-jpq/coq_nvim/blob/coq/coq/server/registrants/options.py#L65

EDIT: Basically, I have the opposite problem of this person: https://vi.stackexchange.com/questions/19971/ctrl-n-should-not-insert-text . I want ctrl+n to insert the text (which it does in normal vim).

I think that StackExchange answer is wrong. i_CTRL-P and i_CTRL-N always insert the word, even when with noinsert.

Also I think this is what prevents the selected suggestion from being inserted:

https://github.com/ms-jpq/coq_nvim/blob/fc6fa8a3cf91858dcd81e9771f0a6d69284be81c/coq/server/trans.py#L121

And fuzzy completion requires this.

Does fuzzy completion in coq require this? Coc and compe.nvim have these filled in and also do fuzzy completion right?

Probably related: https://github.com/ms-jpq/coq_nvim/issues/39#issuecomment-901740679

Maybe immediately inserting interferes with nvim_buf_lines_event.

Related https://github.com/hrsh7th/nvim-cmp/issues/116

Also I think this is what prevents the selected suggestion from being inserted:

https://github.com/ms-jpq/coq_nvim/blob/fc6fa8a3cf91858dcd81e9771f0a6d69284be81c/coq/server/trans.py#L121

And fuzzy completion requires this.

Does fuzzy completion in coq require this? Coc and compe.nvim have these filled in and also do fuzzy completion right?

yes it does, because it can change text that is before where ur cursor is located.

vim's way only really works for updating text after ur cursor.

it kills the fuzziness if you cant update text before the cursor, it just goes back to requiring exact amount of prefix chars

+1

Also I think this is what prevents the selected suggestion from being inserted: https://github.com/ms-jpq/coq_nvim/blob/fc6fa8a3cf91858dcd81e9771f0a6d69284be81c/coq/server/trans.py#L121

And fuzzy completion requires this.

Does fuzzy completion in coq require this? Coc and compe.nvim have these filled in and also do fuzzy completion right?

yes it does, because it can change text that is before where ur cursor is located.

vim's way only really works for updating text after ur cursor.

it kills the fuzziness if you cant update text before the cursor, it just goes back to requiring exact amount of prefix chars

Hi @ms-jpq, I'm not sure if I understand the problem. This works in compe:

I'm quite used to this way of working/typing. Could this maybe be implemented behind an option in coq? I'm very impressed by the speed and typo resistant behaviour, so would like to use it.

Cheers, Hans

@HansPinckaers ,

notice how in the gif the position of the popup doesn't change, even as the cursor moves forward.

this is the "trick", to supporting setting word="<not an empty string>", because for whatever values you put in word, it cannot affect things located before where the popup menu is opened.

---

This brings up the problem that if coq were to support this, it must find the leftest position out of all the potential edits, to plot down the popup menu.

because coq has to support edits that affect content arbitrarily before the position of the cursor, so it makes it impossible to just pick a consistent position, because even as you type, and your cursor naturally moves to the right, the left most position of popup menu can actually move more to the left.

---

why does coq need to support arbitrary edits? because its both in the LSP specs, and needed for Tabnine.

in fact, coq was designed with Tabnine as an equal citizen to LSP.

not that I found Tabnine super useful, but because I found Tabnine's protocol kinda interesting.

Literally every edit under tabnine can affect an arbitrary range both before and after where your cursor is located, and locates your cursor at the same time.

It is much better than how the LSP protocol handles things, where if you want to move the cursor, you have to send in a snippet

Hi @ms-jpq, thanks now I get it! It's a really cool approach. I wonder if we can mimic the behaviour by showing a floating window with the new text on top of the range that is gonna change?

that is a really good idea!,

but I don't think its possible to get the syntax highlight to match up though.

the syntax parsers will have no context to work with, and will mis-highlight.

Ah good point! I guess for regex based highlighting it would be fine. But treesitter may be more difficult.

Maybe for new text that doesn't span multiple lines virtual text can also be a solution.

This is likely the feature that would enable the preview for an arbitrary range.