Julian / Julian/lean.nvim

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

Open
#257 0 comments 0 reactions 0 assignees View on GitHub
enhancement infoview
Dominant language
Lua
Stars
581
Forks
60
Avg merge
4d 12h
Merged PRs (30d)
2

Description

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 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.

Contributor guide

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.