leanprover
[Mouseover pop-up] show type above error
In VSCode, when mousing over a constant, it shows
- First any errors on that constant
- Below it the type of the constant
Now the error is already easily visible in the Lean Infoview, either in the Messages or All Messages tab. Therefore, when mousing over a term, I am never interested in seeing the error. However, the type of a constant is not as easily accessible elsewhere, and very often I want to see the type of the constant (usually to find out which arguments are explicit).
Therefore my suggestion: show the type of the constant above the error in the mouse-over pop-up. It will save me a bit of scrolling time, because the error is often larger than the pop-up. This is a minor issue, but it happens very frequently.
In the Zulip thread there is significant support.
I don't think that we can adjust this. The order of content in hovers is hardcoded in VS Code: https://github.com/microsoft/vscode/blob/d374d10eea0154ce74b5cafe64d3e0096dd58717/src/vs/editor/contrib/hover/browser/markerHoverParticipant.ts#L57 https://github.com/microsoft/vscode/blob/d374d10eea0154ce74b5cafe64d3e0096dd58717/src/vs/editor/contrib/hover/browser/contentHover.ts#L55
