From 84f8871c3fd59a424da2f4ebe8bd5b9be0915b15 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Thu, 25 Jul 2024 10:58:49 +0200 Subject: [PATCH] fix: filter duplicate subexpressions (#4786) 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. --- src/Lean/PrettyPrinter/Parenthesizer.lean | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index f2509edd85..bb01b19be3 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -350,15 +350,17 @@ def term.parenthesizer : CategoryParenthesizer | prec => do maybeParenthesize `term true wrapParens prec $ parenthesizeCategoryCore `term prec where - /-- Wraps the term `stx` in parentheses and then copies its `SourceInfo` to the result. - The purpose of this is to copy synthetic delaborator positions from the `stx` node to the parentheses node, - which causes the info view to view both of these nodes as referring to the same expression. - If we did not copy info, the info view would consider the parentheses to belong to the outer term. + /-- Wraps the term `stx` in parentheses and then moves its `SourceInfo` to the result. + The purpose of this is to move synthetic delaborator positions from the `stx` node to the parentheses node, + which causes the info view to view the node with parentheses as referring to the parenthesized expression. + If we did not move info, the info view would consider the parentheses to belong to the outer term. 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