lean.nvim
lean.nvim copied to clipboard
Julian
neovim support for the Lean theorem prover
For example, Julia REPL supports entering Unicode chars via, e.g., `\alpha` -> `α` or `\:beer:` -> `🍺`, which looks quite similar to Lean. (You can see a full list [here](https://github.com/nvim-telescope/telescope-symbols.nvim/blob/master/data/telescope-sources/julia.json),...
- [ ] Provide a unified API for (re)-configuring sub-functionality, rather than ad hoc functions like `infoview.set_autoopen`. Inspiration probably can be taken from` vim.diagnostic.config` (i.e. we probably should use a...
There are a number of neovim-based GUIs. Some notable ones are: [uivonim](https://github.com/smolck/uivonim) [vimr](https://github.com/qvacua/vimr) [gnvim](https://github.com/vhakulinen/gnvim) [vv](https://github.com/vv-vim/vv) and likely more, given I don't personally stay too much on top of these. The...
Didn't manage to add this in #138: > What's missing is the "show tooltip when moving the cursor over a term" feature (right now you still need to click). From...
Contrary to how I did this in #35, I think rather than switching between per-window and per-tab, we should always allow both, and always initialize a per-tab infoview on new...
Following #126, when an infoview is closed, it should notify its info, which will keep track of how many visible infoviews it is attached to. If that number goes to...
When opening a new tab, right now we always create a new info, but we should have an option that can enable using the same info in a new infoview....
Especially in light of #118 and #113, it would be incredibly useful to give nvim some awareness of how infoview messages are fundamentally structured. This could also address some of...
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`](https://github.com/neovim/neovim/blob/222cd43222c68ba5376b681d2a5fd7b90da138b0/runtime/lua/vim/lsp.lua#L893). Following #113, it should...
When the client has no connection to the lean server, it'd probably be nice if that was persistently shown in the infoview instead of just being in `:messages`. Relates to...