Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support pinnable infoview messages #84

Closed
rish987 opened this issue Jul 5, 2021 · 1 comment · Fixed by #113
Closed

Support pinnable infoview messages #84

rish987 opened this issue Jul 5, 2021 · 1 comment · Fixed by #113
Labels
enhancement New feature or request infoview Relates to infoview

Comments

@rish987
Copy link
Collaborator

rish987 commented Jul 5, 2021

Similar to VSCode, it should be possible to pin/unpin infoview messages.

VSCode seems to support "live" messages that are automatically updated as the surrounding code changes. To me this seems a bit unexpected, and I would prefer to just have pinned messages be permanently "paused" and only update when specifically requested. Not to mention this would make the code simpler. Obviously if someone wants to simulate live updates this could be done with autocmds. Though keep in mind I don't have as much experience writing Lean code myself as reading it, so do let me know if there are other opinions.

@rish987
Copy link
Collaborator Author

rish987 commented Aug 5, 2021

Update: see neovim/neovim#15276 -- basically I think we should closely follow the way things are done at VSCode, which is to update pin positions on textDocument/didChange, rather than doing things ad-hoc with nvim_buf_attach() (the analogue of which was the case in VSCode before leanprover/vscode-lean4#30). This will guarantee that the call to infoview.__update() following updating the pin positions will come after actually having notified the server of the buffer changes.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request infoview Relates to infoview
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant