search

Julian / lean.nvim

Neovim support for the Lean theorem prover
MIT License
277 stars 26 forks source link

Debouncing is negated because of infoview updates #115

Closed rish987 closed 4 months ago

rish987 commented 3 years ago

At the moment, debouncing text changes is kind of pointless, since we're updating the infoview (and hence making a request) on CursorMovedI, which will force textDocument/didChange.

Following #113, it should be safe to remove CursorMovedI entirely, because we'll be updating on textDocument/didChange, and moving the cursor entirely within insert mode without changing the text seems to be a misuse of vim anyways (from my experience, but let me know if I'm wrong about this).

rish987 commented 3 years ago

Correction: I think we should replace CursorMovedI with InsertEnter to allow for things like normal commands A/I and insert mode command <C-o>... to update the infoview. CursorMovedI just seems like something best avoided if possible, it could get called too often with too many other things happening. We would have a similar issue with CursorHoldI if the debounce timer is longer than the hold timer.

rish987 commented 3 years ago

Actually, the above would likely involve adding something like a current field to the current pin so that we would know to update the position in addition to making an update, which I really wanted to avoid doing (i.e. not give special status to the current pin). So I think the best way here is to keep things as is, but make yet another upstream change that configurably allows client.request to abort postpone a request rather than flushing changes. Will try this out with #113 soon.

rish987 commented 3 years ago

(considering this a bug rather than enhancement since people should expect setting debounce_text_changes to work regardless of the timeout.)