max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: review

Browse source
This commit is contained in:
E.W.Ayers 2022-10-16 16:19:37 +01:00 • committed by Gabriel Ebner
parent c9a26596dc
commit 46112a5f2a
1 changed files with 3 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Lean/Server/CodeActions.lean
View file

@ -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