Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix: filter duplicate subexpressions #4786

Merged
merged 3 commits into from
Jul 25, 2024
Merged

fix: filter duplicate subexpressions #4786

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
5e47f96
fix: filter duplicate subexpressions
mhuisi Jul 19, 2024
5f23096
Revert "fix: filter duplicate subexpressions"
mhuisi Jul 19, 2024
a356207
fix: duplicate subexpression info
mhuisi Jul 19, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 7 additions & 5 deletions src/Lean/PrettyPrinter/Parenthesizer.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading