From aea8e11d4ba585f74bbe5cd569b2f007751b451c Mon Sep 17 00:00:00 2001
From: Marc Huisinga <mhuisi@protonmail.com>
Date: Wed, 18 Jun 2025 20:00:20 +0200
Subject: [PATCH] fix: restore code action incrementality (#8868)

This PR ensures that code actions do not have to wait for the full file
to elaborate. This regression was accidentally introduced in #7665.
---
 src/Lean/Server/CodeActions/UnknownIdentifier.lean | 2 +-
 src/Lean/Server/FileWorker/RequestHandling.lean    | 2 +-
 src/Lean/Server/Requests.lean                      | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Server/CodeActions/UnknownIdentifier.lean b/src/Lean/Server/CodeActions/UnknownIdentifier.lean
index eec86834e4..80406aa02a 100644
--- a/src/Lean/Server/CodeActions/UnknownIdentifier.lean
+++ b/src/Lean/Server/CodeActions/UnknownIdentifier.lean
@@ -25,7 +25,7 @@ def waitUnknownIdentifierRanges (doc : EditableDocument) (requestedRange : Strin
   let text := doc.meta.text
   let some parsedSnap := RequestM.findCmdParsedSnap doc requestedRange.start |>.get
     | return #[]
-  let msgLog := Language.toSnapshotTree parsedSnap |>.collectMessagesInRange requestedRange |>.get
+  let msgLog := Language.toSnapshotTree parsedSnap.elabSnap |>.collectMessagesInRange requestedRange |>.get
   let mut ranges := #[]
   for msg in msgLog.unreported do
     if ! msg.data.hasTag (· == unknownIdentifierMessageTag) then
diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean
index 588d6ef5da..c4b7657fd7 100644
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -269,7 +269,7 @@ def findGoalsAt? (doc : EditableDocument) (hoverPos : String.Pos) : ServerTask (
   let text := doc.meta.text
   findCmdParsedSnap doc hoverPos |>.bindCostly fun
     | some cmdParsed =>
-      let t := toSnapshotTree cmdParsed |>.foldSnaps [] fun snap oldGoals => Id.run do
+      let t := toSnapshotTree cmdParsed.elabSnap |>.foldSnaps [] fun snap oldGoals => Id.run do
         let some stx := snap.stx?
           | return .pure (oldGoals, .proceed (foldChildren := false))
         let some (pos, tailPos, trailingPos) := getPositions stx
diff --git a/src/Lean/Server/Requests.lean b/src/Lean/Server/Requests.lean
index c2af41ac50..cf2878a5a8 100644
--- a/src/Lean/Server/Requests.lean
+++ b/src/Lean/Server/Requests.lean
@@ -394,7 +394,7 @@ def findCmdDataAtPos
     (includeStop : Bool)
     : ServerTask (Option (Syntax × Elab.InfoTree)) :=
   findCmdParsedSnap doc hoverPos |>.bindCheap fun
-    | some cmdParsed => toSnapshotTree cmdParsed |>.findInfoTreeAtPos doc.meta.text hoverPos includeStop |>.bindCheap fun
+    | some cmdParsed => toSnapshotTree cmdParsed.elabSnap |>.findInfoTreeAtPos doc.meta.text hoverPos includeStop |>.bindCheap fun
       | some infoTree => .pure <| some (cmdParsed.stx, infoTree)
       | none          => cmdParsed.elabSnap.infoTreeSnap.task.asServerTask.mapCheap fun s =>
         assert! s.infoTree?.isSome