From 46112a5f2af57bc2fb9fc319e8175f0cc36703f8 Mon Sep 17 00:00:00 2001
From: "E.W.Ayers" <edward.ayers@outlook.com>
Date: Sun, 16 Oct 2022 16:19:37 +0100
Subject: [PATCH] fix: review

---
 src/Lean/Server/CodeActions.lean | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Server/CodeActions.lean b/src/Lean/Server/CodeActions.lean
index 5fa4717071..1cb1a29717 100644
--- a/src/Lean/Server/CodeActions.lean
+++ b/src/Lean/Server/CodeActions.lean
@@ -104,17 +104,16 @@ def handleCodeAction (params : CodeActionParams) : RequestM (RequestTask (Array
         let names := codeActionProviderExt.getState env |>.toArray
         let caps ← names.mapM evalCodeActionProvider
         return Array.zip names caps
-      caps.concatMapM (fun (providerName, cap) => do
+      caps.concatMapM fun (providerName, cap) => do
         let cas ← cap params snap
-        cas.mapIdxM (fun i lca => do
+        cas.mapIdxM fun i lca => do
+          if lca.lazy?.isNone then return lca.eager
           let data : CodeActionResolveData := {
             params, providerName, providerResultIndex := i
           }
           let j : Json := toJson data
           let ca := { lca.eager with data? := some j }
           return ca
-        )
-      )
 
 builtin_initialize
   registerLspRequestHandler "textDocument/codeAction" CodeActionParams (Array CodeAction) handleCodeAction