From b41037d7ed00f3c2af29d82fede3bacf4605d41b Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Fri, 4 Aug 2023 17:02:50 +0200 Subject: [PATCH] Corrected the diagnostics and feedbacks api which was wonky, - Seperated feedbacks and diagnostics instead of returning a pair --- language-server/dm/documentManager.ml | 21 +++++++++++++-------- language-server/dm/documentManager.mli | 6 +++++- language-server/lsp/extProtocol.ml | 2 +- language-server/tests/common.ml | 8 ++++---- language-server/vscoqtop/lspManager.ml | 5 +++-- 5 files changed, 26 insertions(+), 16 deletions(-) diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml index 01848dbe..44c11e65 100644 --- a/language-server/dm/documentManager.ml +++ b/language-server/dm/documentManager.ml @@ -126,23 +126,29 @@ let make_coq_feedback doc range oloc message channel = in CoqFeedback.{ range; message; channel } -let feedbacks_and_diagnostics st = +let feedbacks st = + let all_feedback = ExecutionManager.feedback st.execution_state in + (* we are resilient to a state where invalidate was not called yet *) + let exists (id,_) = Option.has_some (Document.get_sentence st.document id) in + let notices_debugs_infos (id, (lvl, oloc, msg)) = Option.map (fun lvl -> id, (lvl, oloc, msg)) (FeedbackChannel.t_of_feedback_level lvl) in + let feedbacks = all_feedback |> List.filter exists |> List.filter_map notices_debugs_infos in + let mk_coq_fb (id, (lvl, oloc, msg)) = + make_coq_feedback st.document (Document.range_of_id st.document id) oloc msg lvl + in + List.map mk_coq_fb feedbacks + +let diagnostics st = let parse_errors = Document.parse_errors st.document in let all_exec_errors = ExecutionManager.errors st.execution_state in let all_feedback = ExecutionManager.feedback st.execution_state in (* we are resilient to a state where invalidate was not called yet *) let exists (id,_) = Option.has_some (Document.get_sentence st.document id) in let exec_errors = all_exec_errors |> List.filter exists in - let notices_debugs_infos (id, (lvl, oloc, msg)) = Option.map (fun lvl -> id, (lvl, oloc, msg)) (FeedbackChannel.t_of_feedback_level lvl) in let warnings_and_errors (id, (lvl, oloc, msg)) = Option.map (fun lvl -> id, (lvl, oloc, msg)) (Severity.t_of_feedback_level lvl) in let diags = all_feedback |> List.filter exists |> List.filter_map warnings_and_errors in - let feedbacks = all_feedback |> List.filter exists |> List.filter_map notices_debugs_infos in let mk_diag (id,(lvl,oloc,msg)) = make_diagnostic st.document (Document.range_of_id st.document id) oloc msg lvl in - let mk_coq_fb (id, (lvl, oloc, msg)) = - make_coq_feedback st.document (Document.range_of_id st.document id) oloc msg lvl - in let mk_error_diag (id,(oloc,msg)) = mk_diag (id,(Severity.Error,oloc,msg)) in let mk_parsing_error_diag Document.{ msg = (oloc,msg); start; stop } = let doc = Document.raw_document st.document in @@ -154,8 +160,7 @@ let feedbacks_and_diagnostics st = in List.map mk_parsing_error_diag parse_errors @ List.map mk_error_diag exec_errors @ - List.map mk_diag diags, - List.map mk_coq_fb feedbacks + List.map mk_diag diags let reset { uri; opts; init_vs; document; execution_state } = let text = RawDocument.text @@ Document.raw_document document in diff --git a/language-server/dm/documentManager.mli b/language-server/dm/documentManager.mli index 01be4983..a6d6d52e 100644 --- a/language-server/dm/documentManager.mli +++ b/language-server/dm/documentManager.mli @@ -75,10 +75,14 @@ val executed_ranges : state -> exec_overview val observe_id_range : state -> Lsp.LspData.Range.t option (** returns the range of the sentence referenced by observe_id **) -val feedbacks_and_diagnostics : state -> Diagnostic.t list * CoqFeedback.t list +val diagnostics : state -> Diagnostic.t list (** diagnostics [doc] returns the diagnostics corresponding to the sentences that have been executed in [doc]. *) +val feedbacks : state -> CoqFeedback.t list +(** feedback [doc] returns notice, info and debug level feedbacks from coq corresponding + to the sentences that have been executed in [doc]. *) + val get_proof : state -> Position.t option -> Lsp.ProofState.t option val get_completions : state -> Position.t -> (completion_item list, string) Result.t diff --git a/language-server/lsp/extProtocol.ml b/language-server/lsp/extProtocol.ml index 878d8e90..47546b8e 100644 --- a/language-server/lsp/extProtocol.ml +++ b/language-server/lsp/extProtocol.ml @@ -105,7 +105,7 @@ module Notification = struct type t = { uri: Uri.t; - feedback: CoqFeedback.t list + feedbacks: CoqFeedback.t list }[@@deriving yojson] end diff --git a/language-server/tests/common.ml b/language-server/tests/common.ml index c6252b56..ddfdcded 100644 --- a/language-server/tests/common.ml +++ b/language-server/tests/common.ml @@ -149,11 +149,11 @@ type feedback_spec = | F of sentence_id * Lsp.LspData.FeedbackChannel.t * string let check_no_diag st = - let diagnostics, _ = DocumentManager.feedbacks_and_diagnostics st in + let diagnostics = DocumentManager.diagnostics st in [%test_pred: Lsp.LspData.Diagnostic.t list] List.is_empty diagnostics let check_no_feedback st = - let _, feedbacks = DocumentManager.feedbacks_and_diagnostics st in + let feedbacks = DocumentManager.feedbacks st in [%test_pred: Lsp.LspData.CoqFeedback.t list] List.is_empty feedbacks let check_diag st specl = @@ -168,7 +168,7 @@ let check_diag st specl = Caml.(=) severity s && Str.string_match (Str.regexp rex) message 0 in - let diagnostics, _ = DocumentManager.feedbacks_and_diagnostics st in + let diagnostics = DocumentManager.diagnostics st in let diagnostics = List.map ~f:fix_diagnostic diagnostics in run @@ map_error ~f:(fun s -> Printf.sprintf "%s\n\nDiagnostics: %s" s ( @@ -197,7 +197,7 @@ let check_feedback st specl = Caml.(=) channel s && Str.string_match (Str.regexp rex) message 0 in - let _, feedbacks = DocumentManager.feedbacks_and_diagnostics st in + let feedbacks = DocumentManager.feedbacks st in let feedbacks = List.map ~f:fix_feedback feedbacks in run @@ map_error ~f:(fun s -> Printf.sprintf "%s\n\nCoq Feedbacks: %s" s ( diff --git a/language-server/vscoqtop/lspManager.ml b/language-server/vscoqtop/lspManager.ml index 7accd641..ecef8d6e 100644 --- a/language-server/vscoqtop/lspManager.ml +++ b/language-server/vscoqtop/lspManager.ml @@ -161,7 +161,8 @@ let parse_loc json = Position.{ line ; character } let publish_feedbacks_and_diagnostics uri doc = - let diagnostics, feedback = Dm.DocumentManager.feedbacks_and_diagnostics doc in + let diagnostics = Dm.DocumentManager.diagnostics doc in + let feedbacks = Dm.DocumentManager.feedbacks doc in let diag_notification = Protocol.Notification.Server.PublishDiagnostics { uri; diagnostics @@ -169,7 +170,7 @@ let publish_feedbacks_and_diagnostics uri doc = in let fb_notification = ExtProtocol.Notification.Server.PublishCoqFeedback { uri; - feedback + feedbacks } in output_jsonrpc @@ Notification Protocol.Notification.Server.(jsonrpc_of_t diag_notification);