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

Send a message instead of crashing when filename is invalid. #696

Merged
merged 1 commit into from
Nov 30, 2023
Merged

Send a message instead of crashing when filename is invalid. #696

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
6 changes: 4 additions & 2 deletions language-server/dm/documentManager.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -230,9 +230,11 @@ let validate_document state =

let init init_vs ~opts uri ~text =
Vernacstate.unfreeze_full_state init_vs;
let top = Coqargs.(dirpath_of_top (TopPhysical (DocumentUri.to_path uri))) in
let top = try Coqargs.(dirpath_of_top (TopPhysical (DocumentUri.to_path uri))) with
e -> raise e
in
Coqinit.start_library ~top opts;
let init_vs = Vernacstate.freeze_full_state () in
let init_vs = Vernacstate.freeze_full_state () in
let document = Document.create_document init_vs.Vernacstate.synterp text in
let execution_state, feedback = ExecutionManager.init init_vs in
let st = { uri; opts; init_vs; document; execution_state; observe_id = None } in
Expand Down
16 changes: 14 additions & 2 deletions language-server/vscoqtop/lspManager.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -199,6 +199,12 @@ let send_move_cursor uri range =
let notification = Notification.Server.MoveCursor {uri;range} in
output_notification notification

let send_error_notification message =
let type_ = MessageType.Error in
let params = ShowMessageParams.{type_; message} in
let notification = Lsp.Server_notification.ShowMessage params in
output_json @@ Jsonrpc.Notification.yojson_of_t @@ Lsp.Server_notification.to_jsonrpc notification

let update_view uri st =
if (Dm.ExecutionManager.is_diagnostics_enabled ()) then (
send_highlights uri st;
Expand All @@ -219,7 +225,9 @@ let run_documents () =
let textDocumentDidOpen params =
let Lsp.Types.DidOpenTextDocumentParams.{ textDocument = { uri; text } } = params in
let vst, opts = get_init_state () in
let st, events = Dm.DocumentManager.init vst ~opts uri ~text in
let st, events = try Dm.DocumentManager.init vst ~opts uri ~text with
e -> raise e
in
let (st, events') =
if !check_mode = Settings.Mode.Continuous then
Dm.DocumentManager.interpret_in_background st
Expand Down Expand Up @@ -466,7 +474,11 @@ let dispatch_request : type a. Jsonrpc.Id.t -> a Request.Client.t -> (a,string)
let dispatch_std_notification =
let open Lsp.Client_notification in function
| TextDocumentDidOpen params -> log "Recieved notification: textDocument/didOpen";
textDocumentDidOpen params
begin try textDocumentDidOpen params with
exn -> let info = Exninfo.capture exn in
let message = "Error while opening document. " ^ Pp.string_of_ppcmds @@ CErrors.iprint_no_report info in
send_error_notification message; []
end
| TextDocumentDidChange params -> log "Recieved notification: textDocument/didChange";
textDocumentDidChange params
| TextDocumentDidClose params -> log "Recieved notification: textDocument/didClose";
Expand Down
Loading