diff --git a/src/Lean/Server/FileWorker/Utils.lean b/src/Lean/Server/FileWorker/Utils.lean index 6a6be5897b..558b9ddcf4 100644 --- a/src/Lean/Server/FileWorker/Utils.lean +++ b/src/Lean/Server/FileWorker/Utils.lean @@ -76,8 +76,8 @@ def store (st : RpcSessionState) (typeName : Name) (obj : NonScalar) : Lsp.RpcRe (ref, st') def release (st : RpcSessionState) (ref : Lsp.RpcRef) : Bool × RpcSessionState := - let st' := { st with aliveRefs := st.aliveRefs.erase ref } - (st.aliveRefs.contains ref, st') + let released := st.aliveRefs.contains ref + (released, { st with aliveRefs := st.aliveRefs.erase ref }) end RpcSessionState