RFC: indicator for out of date infoview

[hargoniX]

Proposal

Show some form of indicator for when the goal state that's currently being presented in the info view is out of date / being recomputed.

• User Experience: Users can clearly judge when the information they are being presented is current. With recent features such as incrementality or the planned feature to show goals before the entire proof was elaborated this type of information becomes more important.

• Beneficiaries: People that write large proofs on Lean releases with incrementality etc. know precisely when the information they are looking at is out of date/up to date.

• Maintainability: Unclear.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

[Vtec234]

Have you noticed that a yellow tint appears on the location (myfile.lean:12:34) when it is loading? Are you requesting a more prominent indication?

[hargoniX]

I do think a more prominent indication would be sensible yes. I talked to a few users and none of them (including myself) even noticed that this feature exists, let alone its meaning.