From 5e47f961fb3e33449ce3247a007ddad574daa07f Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Fri, 19 Jul 2024 11:03:53 +0200 Subject: [PATCH 1/3] fix: filter duplicate subexpressions --- src/Lean/Widget/InteractiveCode.lean | 26 ++++++++++++++++---------- 1 file changed, 16 insertions(+), 10 deletions(-) diff --git a/src/Lean/Widget/InteractiveCode.lean b/src/Lean/Widget/InteractiveCode.lean index f29100bd383f..d7a30afae621 100644 --- a/src/Lean/Widget/InteractiveCode.lean +++ b/src/Lean/Widget/InteractiveCode.lean @@ -60,18 +60,24 @@ def SubexprInfo.withDiffTag (tag : DiffTag) (c : SubexprInfo) : SubexprInfo := /-- Tags pretty-printed code with infos from the delaborator. -/ partial def tagCodeInfos (ctx : Elab.ContextInfo) (infos : SubExpr.PosMap Elab.Info) (tt : TaggedText (Nat × Nat)) : CodeWithInfos := - go tt + go tt none where - go (tt : TaggedText (Nat × Nat)) := + go (tt : TaggedText (Nat × Nat)) (parentPos : Option Nat) := tt.rewrite fun (n, _) subTt => - match infos.find? n with - | none => go subTt - | some i => - let t : SubexprInfo := { - info := WithRpcRef.mk { ctx, info := i, children := .empty } - subexprPos := n - } - TaggedText.tag t (go subTt) + if some n == parentPos then + -- Filters a subexpression if its position is identical to that of its parent. + -- This ensures that `(foo)` and its subexpr `foo` do not produce separate subexpressions + -- with the same subexpression position. + go subTt n + else + match infos.find? n with + | none => go subTt n + | some i => + let t : SubexprInfo := { + info := WithRpcRef.mk { ctx, info := i, children := .empty } + subexprPos := n + } + TaggedText.tag t (go subTt n) def ppExprTagged (e : Expr) (explicit : Bool := false) : MetaM CodeWithInfos := do if pp.raw.get (← getOptions) then From 5f23096eea56613a4db90457754b6588c8f38c14 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Fri, 19 Jul 2024 18:50:56 +0200 Subject: [PATCH 2/3] Revert "fix: filter duplicate subexpressions" This reverts commit 5e47f961fb3e33449ce3247a007ddad574daa07f. --- src/Lean/Widget/InteractiveCode.lean | 26 ++++++++++---------------- 1 file changed, 10 insertions(+), 16 deletions(-) diff --git a/src/Lean/Widget/InteractiveCode.lean b/src/Lean/Widget/InteractiveCode.lean index d7a30afae621..f29100bd383f 100644 --- a/src/Lean/Widget/InteractiveCode.lean +++ b/src/Lean/Widget/InteractiveCode.lean @@ -60,24 +60,18 @@ def SubexprInfo.withDiffTag (tag : DiffTag) (c : SubexprInfo) : SubexprInfo := /-- Tags pretty-printed code with infos from the delaborator. -/ partial def tagCodeInfos (ctx : Elab.ContextInfo) (infos : SubExpr.PosMap Elab.Info) (tt : TaggedText (Nat × Nat)) : CodeWithInfos := - go tt none + go tt where - go (tt : TaggedText (Nat × Nat)) (parentPos : Option Nat) := + go (tt : TaggedText (Nat × Nat)) := tt.rewrite fun (n, _) subTt => - if some n == parentPos then - -- Filters a subexpression if its position is identical to that of its parent. - -- This ensures that `(foo)` and its subexpr `foo` do not produce separate subexpressions - -- with the same subexpression position. - go subTt n - else - match infos.find? n with - | none => go subTt n - | some i => - let t : SubexprInfo := { - info := WithRpcRef.mk { ctx, info := i, children := .empty } - subexprPos := n - } - TaggedText.tag t (go subTt n) + match infos.find? n with + | none => go subTt + | some i => + let t : SubexprInfo := { + info := WithRpcRef.mk { ctx, info := i, children := .empty } + subexprPos := n + } + TaggedText.tag t (go subTt) def ppExprTagged (e : Expr) (explicit : Bool := false) : MetaM CodeWithInfos := do if pp.raw.get (← getOptions) then From a3562075acdea4a1bfbcc0b575e709d75e712443 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Fri, 19 Jul 2024 19:21:33 +0200 Subject: [PATCH 3/3] fix: duplicate subexpression info --- 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 f2509edd8574..bb01b19be3e7 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