search

Julian / lean.nvim

neovim support for the Lean theorem prover
MIT License
255 stars 25 forks source link

Add an equivalent of lean4.refreshFileDependencies. #265

Closed Julian closed 2 years ago

Julian commented 2 years ago

Needed for forcibly telling Lean 4 to rebuild dependencies when editing a dependent file.

:e works but requires writing the file, and will refire Buf-related events, which may be undesirable.

Ultimately Lean 4 is hopefully planning to obviate the need to do this manually, but for now this mirrors VSCode.

Closes: #262

gebner commented 2 years ago

The LSP side LGTM.