Merge pull request #1012 from Durbatuluk1701/empty_completion_management

Return empty completions rather than error
coq · Jan 28, 2025 · d5734a0 · d5734a0
2 parents 9af98b0 + fcfffbc
commit d5734a0
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 11 deletions.
diff --git 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
@@ -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
@@ -432,13 +432,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*)