fix: consistently show non-mvar term in hovertext #5368
Conversation
Previously, the hover text would only show the term in the hovertext if the pretty-printed text was 'atomic', which excluded expressions like `1 + 1`. This made the hovertext less useful for inspecting an underscore (`_`), since only the type (and not the term) would be displayed for a complex expression. Change the behavior to hide the term if it's a single metavariable, and otherwise display both the term and type. This ensures that we do not produce unhelpful hovertext like `?m : SomeType` (we still produce just `SomeType`). We now display both the term and type in a few other cases - this makes the output a little more verbose, but also ensures that users can see resolved metavariables in the term. Closes leanprover#5367
Aaron1011
force-pushed
the
hover-underscore
branch
from
ad2abec
to
ace0538
Compare
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
| @@ -316,7 +316,7 @@ where | |||
| if let some ldecl := (← getLCtx).findFVar? e then | |||
| !ldecl.userName.hasMacroScopes | |||
| else false | |||
| else isAtomicFormat eFmt | |||
| else !e.isMVar | |||
There was a problem hiding this comment.
Are you sure that you want to check for isMVar here? What about applications of an MVar to another MVar, for example?
There was a problem hiding this comment.
My thinking is while showing something like ?m : SomeType doesn't really provide any useful information, it's better to err on the side of showing more information about inference for more complicated types.
Applying an MVar to an MVar would come from something like _ _, right? I think it would be useful to be able to explicitly see when Lean isn't able to infer terms for MVars in that kind of expression.
| isAtomicFormat : Format → Bool | ||
| | Std.Format.text _ => true | ||
| | Std.Format.group f _ => isAtomicFormat f | ||
| | Std.Format.nest _ f => isAtomicFormat f | ||
| | Std.Format.tag _ f => isAtomicFormat f | ||
| | _ => false |
There was a problem hiding this comment.
I don't think that we want to delete this in general. It was originally introduced to avoid cluttering the hover panel with information already present below the cursor in non-_ hover cases (e.g. the test cases in 4078.lean) and I would like to retain that.
There was a problem hiding this comment.
Do you want this to still be used in this pr, or just kept around (unused) for future use?
My concern is that this heuristic can result in more-important expressions being hidden from the user - I first noticed this issue when looking at an _ that was inferred to (p - 1) / q, which was harder for me to deduce by hand than if the term was something simpler like p.
There was a problem hiding this comment.
Ideally, the inferred expression would not be hidden away when hovering over _, but is hidden away in all other cases to avoid cluttering the hover panel with redundant information.
Previously, the hover text would only show the term in the hovertext if the pretty-printed text was 'atomic', which excluded expressions like
1 + 1.This made the hovertext less useful for inspecting an underscore (
_), since only the type (and not the term) would be displayed for a complex expression.Change the behavior to hide the term if it's a single metavariable, and otherwise display both the term and type. This ensures that we do not produce unhelpful hovertext like
?m : SomeType(we still produce justSomeType).We now display both the term and type in a few other cases - this makes the output a little more verbose, but also ensures that users can see resolved metavariables in the term.
Closes #5367