search

Julian / lean.nvim

neovim support for the Lean theorem prover
MIT License
233 stars 23 forks source link

Full HTML widget support in a GUI #59

Open Julian opened 3 years ago

Julian commented 3 years ago

There are a number of neovim-based GUIs.

Some notable ones are:

uivonim vimr gnvim vv

and likely more, given I don't personally stay too much on top of these. The first one is likely particularly interesting given it has contributors who are neovim core devs.

We currently support TUI-based widgets, but for more complex ones such as e.g. the sudoku solver which truly rely on HTML rendering, a GUI (with access to a real browser) is needed.

We could attempt to follow something like bracey's model even for terminal nvim by opening an optional browser window which updates not on save but on infoview update.

Julian commented 2 years ago

lean4-infoview is apparently intended to be editor-agnostic, so if this were to be done it seems it's where we should start.