max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: filter duplicate subexpressions (#4786)

Browse source 
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.
This commit is contained in:
Marc Huisinga 2024-07-25 10:58:49 +02:00 • committed by GitHub
parent 93fa9c8837
commit 84f8871c3f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 7 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/Lean/PrettyPrinter/Parenthesizer.lean
View file

@ -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