From 65705c6b143ed8bc634d099ba2433664c94a4300 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Tue, 23 Jan 2024 20:42:44 +1100
Subject: [PATCH] feat: adaptations for leanprover/lean4#3159 (#557)

---
 Std/CodeAction/Basic.lean | 2 +-
 Std/Lean/InfoTree.lean    | 2 +-
 lean-toolchain            | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/Std/CodeAction/Basic.lean b/Std/CodeAction/Basic.lean
index 17f8b2cac8..7302aaa9c5 100644
--- 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
index f0977a19e9..d69450d575 100644
--- 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
index 4eda11be1f..b39e2129f7 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-01-16
+leanprover/lean4:nightly-2024-01-23