Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Return empty completions rather than error #1012

Merged
merged 1 commit into from
Jan 28, 2025
+10 −11
Merged

Return empty completions rather than error #1012

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 7 additions & 3 deletions language-server/dm/documentManager.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"]
Expand Down
2 changes: 1 addition & 1 deletion language-server/dm/documentManager.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
9 changes: 2 additions & 7 deletions language-server/vscoqtop/lspManager.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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*)
Expand Down
Loading