From 18472f0653f7a022e84548f5b4b6cd4a37d17920 Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Tue, 10 Dec 2024 15:28:02 +0100 Subject: [PATCH] feat: add error if document is parsing If the document is parsing, the document should resend the documentProofs request later. --- language-server/vscoqtop/lspManager.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/language-server/vscoqtop/lspManager.ml b/language-server/vscoqtop/lspManager.ml index 792ceda1..f09cf415 100644 --- a/language-server/vscoqtop/lspManager.ml +++ b/language-server/vscoqtop/lspManager.ml @@ -551,8 +551,12 @@ let sendDocumentProofs id params = let uri = textDocument.uri in match Hashtbl.find_opt states (DocumentUri.to_path uri) with | None -> log @@ "[documentProofs] ignoring event on non existent document"; Error({message="Document does not exist"; code=None}), [] - | Some { st } -> let proofs = Dm.DocumentManager.get_document_proofs st in - Ok Request.Client.DocumentProofsResult.{ proofs }, [] + | Some { st } -> + if Dm.DocumentManager.is_parsing st then + Error {code=(Some Jsonrpc.Response.Error.Code.ServerCancelled); message="Parsing not finished"} , [] + else + let proofs = Dm.DocumentManager.get_document_proofs st in + Ok Request.Client.DocumentProofsResult.{ proofs }, [] let workspaceDidChangeConfiguration params = let Lsp.Types.DidChangeConfigurationParams.{ settings } = params in