From 580c21af2f7e93af321f7cd17ac26a1a52b49fdf Mon Sep 17 00:00:00 2001
From: Romain Tetley <romain.tetley@inria.fr>
Date: Wed, 29 Nov 2023 14:32:25 +0100
Subject: [PATCH] Send a message instead of crashing when filename is invalid.

---
 language-server/dm/documentManager.ml  |  6 ++++--
 language-server/vscoqtop/lspManager.ml | 16 ++++++++++++++--
 2 files changed, 18 insertions(+), 4 deletions(-)

diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml
index 62dfd370..5f99060b 100644
--- a/language-server/dm/documentManager.ml
+++ b/language-server/dm/documentManager.ml
@@ -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
diff --git a/language-server/vscoqtop/lspManager.ml b/language-server/vscoqtop/lspManager.ml
index c468b22a..8f1354fd 100644
--- a/language-server/vscoqtop/lspManager.ml
+++ b/language-server/vscoqtop/lspManager.ml
@@ -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;
@@ -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 
@@ -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";