Skip to content

Commit

Permalink
fixed regression
Browse files Browse the repository at this point in the history
  • Loading branch information
@kmill
kmill committed Dec 1, 2024
1 parent d458645 commit 972840a
Show file tree
Hide file tree
Showing 3 changed files with 92 additions and 73 deletions.
7 changes: 7 additions & 0 deletions src/Init/Prelude.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3931,6 +3931,13 @@ def getId : Syntax → Name
| ident _ _ val _ => val
| _ => Name.anonymous

/-- Retrieve the immediate info from the Syntax node. -/
def getInfo? : Syntax → Option SourceInfo
| atom info .. => some info
| ident info .. => some info
| node info .. => some info
| missing => none

/-- Retrieve the left-most node or leaf's info in the Syntax tree. -/
partial def getHeadInfo? : Syntax → Option SourceInfo
| atom info _ => some info
Expand Down
7 changes: 4 additions & 3 deletions src/Lean/PrettyPrinter/Delaborator/Basic.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -236,7 +236,7 @@ to associate the term to the current expression, unless the syntax has a synthet
and associated `Info` already.
-/
def annotateTermInfoUnlessAnnotated (stx : Term) : Delab := do
if let .synthetic ⟨pos⟩ ⟨pos'⟩ := stx.raw.getHeadInfo then
if let some (.synthetic ⟨pos⟩ ⟨pos'⟩) := stx.raw.getInfo? then
if pos == pos' && (← get).infos.contains pos then
return stx
annotateTermInfo stx
Expand Down Expand Up @@ -454,7 +454,7 @@ open SubExpr (Pos PosMap)
open Delaborator (OptionsPerPos topDownAnalyze DelabM)

def delabCore (e : Expr) (optionsPerPos : OptionsPerPos := {}) (delab : DelabM α) :
MetaM (α × PosMap Elab.Info) := do
MetaM (α × PosMap Elab.Info) := do
/- Using `erasePatternAnnotations` here is a bit hackish, but we do it
`Expr.mdata` affects the delaborator. TODO: should we fix that? -/
let e ← Meta.erasePatternRefAnnotations e
Expand All @@ -474,7 +474,8 @@ def delabCore (e : Expr) (optionsPerPos : OptionsPerPos := {}) (delab : DelabM
topDownAnalyze e
else pure optionsPerPos
let (stx, {infos := infos, ..}) ← catchInternalId Delaborator.delabFailureId
(delab
-- Clear the ref to ensure that quotations in delaborators start with blank source info.
(MonadRef.withRef .missing delab
{ optionsPerPos := optionsPerPos
currNamespace := (← getCurrNamespace)
openDecls := (← getOpenDecls)
Expand Down
151 changes: 81 additions & 70 deletions tests/lean/interactive/Diff.lean.expected.out
View file
Original file line number Diff line number Diff line change
@@ -1,18 +1,20 @@
{ goals := #[{ type := Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0", diffStatus? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0/0/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "x"),
Lean.Widget.TaggedText.text " = ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/0/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "x")]),
Lean.Widget.TaggedText.text " → ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "True")],
{ goals := #[{ type := Lean.Widget.TaggedText.tag
{ subexprPos := "/", diffStatus? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0", diffStatus? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0/0/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "x"),
Lean.Widget.TaggedText.text " = ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/0/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "x")]),
Lean.Widget.TaggedText.text " → ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "True")]),
isInserted? := some false,
isRemoved? := none,
hyps := #[{ type := Lean.Widget.TaggedText.tag
Expand All @@ -22,21 +24,23 @@
isInserted? := some true,
isRemoved? := none }] }] }

{ goals := #[{ type := Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0", diffStatus? := some "willDelete" }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0/0/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "x"),
Lean.Widget.TaggedText.text " = ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/0/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "x")]),
Lean.Widget.TaggedText.text " → ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "True")],
{ goals := #[{ type := Lean.Widget.TaggedText.tag
{ subexprPos := "/", diffStatus? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0", diffStatus? := some "willDelete" }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0/0/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "x"),
Lean.Widget.TaggedText.text " = ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/0/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "x")]),
Lean.Widget.TaggedText.text " → ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "True")]),
isInserted? := some false,
isRemoved? := none,
hyps := #[{ type := Lean.Widget.TaggedText.tag
Expand All @@ -59,19 +63,22 @@
(Lean.Widget.TaggedText.text "Nat"),
Lean.Widget.TaggedText.text "), ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1/0", diffStatus? := some "willDelete" }
{ subexprPos := "/1", diffStatus? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/1/0/0/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "x"),
Lean.Widget.TaggedText.text " = ",
{ subexprPos := "/1/0", diffStatus? := some "willDelete" }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/1/0/0/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "x"),
Lean.Widget.TaggedText.text " = ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1/0/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "x")]),
Lean.Widget.TaggedText.text " → ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1/0/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "x")]),
Lean.Widget.TaggedText.text " → ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "True")]),
{ subexprPos := "/1/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "True")])]),
isInserted? := some false,
isRemoved? := none,
hyps := #[] }] }
Expand All @@ -93,21 +100,23 @@
names := #["x", "y"],
isInserted? := none,
isRemoved? := none },
{ type := Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0", diffStatus? := none }
(Lean.Widget.TaggedText.text "α"),
Lean.Widget.TaggedText.text " → ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1", diffStatus? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/1/0/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "x"),
Lean.Widget.TaggedText.text " = ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1/1", diffStatus? := some "willChange" }
(Lean.Widget.TaggedText.text "y")])],
{ type := Lean.Widget.TaggedText.tag
{ subexprPos := "/", diffStatus? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0", diffStatus? := none }
(Lean.Widget.TaggedText.text "α"),
Lean.Widget.TaggedText.text " → ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1", diffStatus? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/1/0/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "x"),
Lean.Widget.TaggedText.text " = ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1/1", diffStatus? := some "willChange" }
(Lean.Widget.TaggedText.text "y")])]),
names := #["f"],
isInserted? := none,
isRemoved? := none },
Expand Down Expand Up @@ -142,21 +151,23 @@
names := #["x", "y"],
isInserted? := none,
isRemoved? := none },
{ type := Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0", diffStatus? := none }
(Lean.Widget.TaggedText.text "α"),
Lean.Widget.TaggedText.text " → ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1", diffStatus? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/1/0/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "x"),
Lean.Widget.TaggedText.text " = ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1/1", diffStatus? := some "wasChanged" }
(Lean.Widget.TaggedText.text "x")])],
{ type := Lean.Widget.TaggedText.tag
{ subexprPos := "/", diffStatus? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0", diffStatus? := none }
(Lean.Widget.TaggedText.text "α"),
Lean.Widget.TaggedText.text " → ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1", diffStatus? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/1/0/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "x"),
Lean.Widget.TaggedText.text " = ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1/1", diffStatus? := some "wasChanged" }
(Lean.Widget.TaggedText.text "x")])]),
names := #["f"],
isInserted? := none,
isRemoved? := none },
Expand Down

0 comments on commit 972840a

Please sign in to comment.