search

Julian / lean.nvim

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

Make it easier to notice when a document is still processing for diagnostics #252

Closed Julian closed 2 years ago

Julian commented 2 years ago

Right now, running e.g. vim.diagnostic.goto_next() will silently succeed if the file is still processing (and therefore has no diagnostics).

I'm not sure we can fully hook into doing this, but it might be nice if there was an easy way to have things fail until/unless the document is fully processed, as I (and probably others) sometimes use vim.diagnostic.goto_next as a poor-man's "is there anything to fix in this file".

Julian commented 2 years ago

Ok erroring I think is indeed not possible without a wrapper but the obvious solution here is probably to just set a diagnostic at the top of the processing region (and move/remove it as processing continues).