From fcfffbcfb76f5530a68db25661955ab3b55909ee Mon Sep 17 00:00:00 2001
From: Will Thomas <30wthomas@gmail.com>
Date: Mon, 27 Jan 2025 22:06:18 -0700
Subject: [PATCH] Return empty completions rather than error

---
 language-server/dm/documentManager.ml  | 10 +++++++---
 language-server/dm/documentManager.mli |  2 +-
 language-server/vscoqtop/lspManager.ml |  9 ++-------
 3 files changed, 10 insertions(+), 11 deletions(-)

diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml
index ea7a9ae5a..5043a53c4 100644
--- a/language-server/dm/documentManager.ml
+++ b/language-server/dm/documentManager.ml
@@ -667,13 +667,17 @@ let get_context st pos = context_of_id st (id_of_pos st pos)
 
 let get_completions st pos =
   match id_of_pos st pos with
-  | None -> Error ("Can't get completions, no sentence found before the cursor")
+  | None -> 
+      log ("Can't get completions, no sentence found before the cursor");
+      []
   | Some id ->
     let ost = ExecutionManager.get_vernac_state st.execution_state id in
     let settings = ExecutionManager.get_options () in
     match Option.bind ost @@ CompletionSuggester.get_completions settings.completion_options with
-    | None -> Error ("Can't get completions")
-    | Some lemmas -> Ok (lemmas)
+    | None -> 
+        log "No completions available";
+        []
+    | Some lemmas -> lemmas
 
 [%%if coq = "8.18" || coq = "8.19"]
 [%%elif coq = "8.20"]
diff --git a/language-server/dm/documentManager.mli b/language-server/dm/documentManager.mli
index dff6d16e4..d7cc35716 100644
--- a/language-server/dm/documentManager.mli
+++ b/language-server/dm/documentManager.mli
@@ -118,7 +118,7 @@ val all_diagnostics : state -> Diagnostic.t list
 
 val get_proof : state -> Settings.Goals.Diff.Mode.t -> sentence_id option -> ProofState.t option
 
-val get_completions : state -> Position.t -> (completion_item list, string) Result.t
+val get_completions : state -> Position.t -> completion_item list 
 
 val handle_event : event -> state -> block:bool -> Settings.Mode.t -> Settings.Goals.Diff.Mode.t -> handled_event
 (** handles events and returns a new state if it was updated. On top of the next events, it also returns info
diff --git a/language-server/vscoqtop/lspManager.ml b/language-server/vscoqtop/lspManager.ml
index 7990a7b7a..1f412b45c 100644
--- a/language-server/vscoqtop/lspManager.ml
+++ b/language-server/vscoqtop/lspManager.ml
@@ -458,13 +458,8 @@ let textDocumentCompletion id params =
   match Hashtbl.find_opt states (DocumentUri.to_path uri) with
   | None -> log @@ "[textDocumentCompletion]ignoring event on non existent document"; Error( {message="Document does not exist"; code=None} ), []
   | Some { st } -> 
-    match Dm.DocumentManager.get_completions st position with
-    | Ok completionItems -> 
-      let items = List.mapi make_CompletionItem completionItems in
-      return_completion ~isIncomplete:false ~items, []
-    | Error e -> 
-      let message = e in
-      Error {message; code=None}, []
+    let items = List.mapi make_CompletionItem (Dm.DocumentManager.get_completions st position) in
+    return_completion ~isIncomplete:false ~items, []
 
 let documentSymbol id params =
   let Lsp.Types.DocumentSymbolParams.{ textDocument = {uri}; partialResultToken; workDoneToken } = params in (*TODO: At some point we might get ssupport for partialResult and workDone*)