Corrected the diagnostics and feedbacks api which was wonky,

- Seperated feedbacks and diagnostics instead of returning a pair

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

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

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

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 (

language-server/vscoqtop/lspManager.ml

@@ -161,15 +161,16 @@ 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
   }
   in
   let fb_notification = ExtProtocol.Notification.Server.PublishCoqFeedback {
     uri; 
-    feedback
+    feedbacks
   }
   in
   output_jsonrpc @@ Notification Protocol.Notification.Server.(jsonrpc_of_t diag_notification);