c46f1e941c
This PR fixes an issue where `let n : Nat := sorry` in the Infoview pretty prints as ``n : ℕ := sorry `«Foo:17:17»``. This was caused by top-level expressions being pretty printed with the same rules as Infoview hovers. Closes #6715. Refactors `Lean.Widget.ppExprTagged`; now it takes a delaborator, and downstream users should configure their own pretty printer option overrides if necessary if they used the `explicit` argument (see `Lean.Widget.makePopup.ppExprForPopup` for an example). Breaking change: `ppExprTagged` does not set `pp.proofs` on the root expression. |
||
|---|---|---|
| .. | ||
| ExampleHover.lean | ||
| InlayHints.lean | ||
| RequestHandling.lean | ||
| SemanticHighlighting.lean | ||
| SetupFile.lean | ||
| Utils.lean | ||
| WidgetRequests.lean | ||