Julian / lean.nvim

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

Make how and when the infoview updates more configurable, particularly for cases when it goes blank #257

Open Julian opened 2 years ago

Julian commented 2 years ago

Putting this here off the back of / in order to track this Zulip request.

I want to be able to configure Infoview updates to be less "jittery" (and possibly then the default should be reconsidered). Often one can be typing things and the infoview will change to be empty, or say processing if that message is enabled, when it would be a lot more useful to continue showing the last infoview contents until the new ones are available.

It occurs to me that it may be cohesive if we introduce the same orange progress bar concept which we use in the sign column for Lean buffers to the infoview window, and thereby indicate "what's here isn't current anymore" not always by removing it, but by instead modifying the infoview window's sign column.

Other ideas are of course welcome, I don't know that I have a perfect one yet, but I know I've been frustrated by similar things that it seems Bartosz is.