fix: filter duplicate subexpressions

[mhuisi]

For every parenthesized expression (foo), the InfoView produces an interactive component both for (foo) itself and its subexpression foo because the corresponding TaggedText in the language server is duplicated as well. Both of these subexpressions have the same subexpression position and so they are identical w.r.t. interactive features.

Removing this duplication would help reduce the size of the DOM of the InfoView and ensure that the UI for InfoView features is consistent for (foo) and foo (e.g. hovers would always highlight (foo), not either (foo) or foo depending on whether the mouse cursor is on the bracket or not). It would also help resolve a bug where selecting a subexpression will yield selection highlighting both for (foo) and foo, as we use the subexpression position to identify which terms to highlight.

This PR adjusts the parenthesizer to move the corresponding info instead of duplicating it.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 7d2155943c67c743409420b4546d47fadf73af1c --onto a94805ff71f7576ee014aafc76b29e29b066bd80. (2024-07-19 09:29:16)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 7d2155943c67c743409420b4546d47fadf73af1c --onto 8ceb24a5e6782aac39fdb3bb2b47021ac38d0847. (2024-07-22 08:46:20)

[Vtec234]

One question before thinking about the details of filtering: why do this here rather than somewhere earlier? Perhaps it should be viewed a bug in the delaborator or somewhere in the pretty-printer that it produces both of these rather than just one?

[kmill]

Here's where the parenthesizer adds parentheses and copies source position from the syntax being parenthesized: https://github.com/leanprover/lean4/blob/master/src/Lean/PrettyPrinter/Parenthesizer.lean#L353-L361

The reason it doesn't delete source position from the syntax is because it's using SourceInfo.fromRef, which is willing to descend into the syntax to find something, and we just didn't implement the algorithm to try to correctly delete source position from the inner expression (being able to hover over the parentheses and getting reasonable behavior was a good enough improvement on its own). Potentially using SourceInfo.fromRef is incorrect here, and it ought to try to only get source position from the syntax node/atom itself, which would make deleting easy.

On the other hand, the filtering approach in the PR might be a way to address that comment in the linked code about why it doesn't use withRef — this PR would keep each parenthesis from being individually hoverable, right?

[mhuisi]

On the other hand, the filtering approach in the PR might be a way to address that comment in the linked code about why it doesn't use withRef — this PR would keep each parenthesis from being individually hoverable, right?

Hovering over the parenthesis will highlight the parentheses and the term inside of it. Hovering on the head of the term inside of it will also highlight the parentheses, whereas before it would only highlight the term, not the parentheses.

[mhuisi]

I believe something like the following would also accomplish the same thing as this PR if I am not mistaken:

index f2509edd85..71451432f3 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -357,8 +357,10 @@ where
   Note: we do not do `withRef stx` because that causes the "(" and ")" tokens to have source info as well,
   causing the info view to highlight each parenthesis as an independent expression. -/
   wrapParens (stx : Syntax) : Syntax := Unhygienic.run do
+    let stxInfo := SourceInfo.fromRef stx
+    let stx := stx.setInfo .none
     let pstx ← `(($(⟨stx⟩)))
-    return pstx.raw.setInfo (SourceInfo.fromRef stx)
+    return pstx.raw.setInfo stxInfo
 
 @[builtin_category_parenthesizer tactic]
 def tactic.parenthesizer : CategoryParenthesizer | prec => do

What do you think?

[kmill]

@mhuisi I think that's an improvement to wrapParens. It's possible that fromRef collects the source position from deeper inside the expression however, so using setInfo .none is technically not sufficient. However, I think if it's not sufficient in particular cases, we can blame particular delaborators for it.

I'd say that if this change to the parenthesizer appears to work, let's go for it.

[mhuisi]

(Kyle signed this off in a PM)