feat: adaptations for leanprover/lean4#3159

leanprover-community · Jan 23, 2024 · b191117 · b191117
1 parent 427cf7e
commit b191117
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git a/Std/CodeAction/Basic.lean b/Std/CodeAction/Basic.lean
@@ -147,7 +147,7 @@ partial def findInfoTree? (kind : SyntaxNodeKind) (tgtRange : String.Range)
   (f : ContextInfo → Info → Bool) (canonicalOnly := false) :
     Option (ContextInfo × InfoTree) :=
   match t with
-  | .context ctx t => findInfoTree? kind tgtRange ctx t f canonicalOnly
+  | .context ctx t => findInfoTree? kind tgtRange (ctx.mergeIntoOuter? ctx?) t f canonicalOnly
   | node@(.node i ts) => do
     if let some ctx := ctx? then
       if let some range := i.stx.getRange? canonicalOnly then

diff --git a/Std/Lean/InfoTree.lean b/Std/Lean/InfoTree.lean
@@ -14,7 +14,7 @@ partial def InfoTree.foldInfo' (init : α) (f : ContextInfo → InfoTree → α
 where
   /-- `foldInfo'.go` is like `foldInfo'` but with an additional outer context parameter `ctx?`. -/
   go ctx? a
-  | context ctx t => go ctx a t
+  | context ctx t => go (ctx.mergeIntoOuter? ctx?) a t
   | t@(node i ts) =>
     let a := match ctx? with
       | none => a

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-01-16
+leanprover/lean4:nightly-2024-01-23