Julian Berman
Julian Berman
Putting this here off the back of / in order to track [this Zulip request](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/lean.2Envim/near/280738234). I want to be able to configure Infoview updates to be less "jittery" (and possibly...
See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Parser.20Expression.20Grammars.20.28PVS.20and.20Lean.20comparison.29/near/279170568 Perhaps a simple thing we could do is just show a horizontal rule (i.e. a line) below any instance of this tactic.
E.g. pass this test: ```lua -- Emitted by e.g. show_term it('replaces redundant term and tactic mode', helpers.clean_buffer([[ namespace tactic.interactive meta def foo (t: itactic) : itactic := (do tactic.trace "Try...
Compare how: ``` import tactic.explode_widget #explode_widget nat.mul_comm ``` looks in VSCode: to what we render which just ends up a wall of text:
When working on mathlib in a case where olean compilation is happening in the background (e.g. with no cache, or whilst working on a lower level file), exiting neovim often...
The infoview assembles a number of subcomponents -- Tactic state, Term state, Diagnostic info, Standard error output, It may be nice to allow some customization here at some point --...
Right now a fugitive buffer from e.g. `Gdiff` on a Lean file does not connect an LSP client to the fugitive window, and therefore doesn't show infoview state.
Add a configuration option `infoview.autoclose = true (default)` which indicates the infoview should be closed if no Lean buffers are updating it anymore (e.g. particularly if it is the last...
- [ ] 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...