Merge pull request #843 from ejgallego/diagnostics_data

[lang] Move `Lang.Diagnostics.Data.t` from a list to name field

CHANGES.md

@@ -34,6 +34,8 @@
    info that is needed is at hand. It could also be tried to set the
    build target for immediate requests to the view hint, but we should
    see some motivation for that (@ejgallego, #841)
+ - [lsp] [diagnostics] (! breaking change) change type of diagnostics
+   extra data from list to named record (@ejgallego, #843)
 
 # coq-lsp 0.2.0: From Green to Blue
 -----------------------------------

etc/doc/PROTOCOL.md

@@ -164,6 +164,20 @@ today we offer two kinds of extra information on errors:
 - range of the full sentence that displayed the error,
 - if the error was on a Require, information about the library that failed.
 
+As of today, this extra data is passed via member parameters
+```typescript
+// From `prefix` Require `refs`
+type failedRequire = {
+    prefix ?: qualid
+    refs : qualid list
+}
+
+type DiagnosticsData = {
+    sentenceRange ?: Range;
+    failedRequire ?: FailedRequire
+}
+```
+
 ### Goal Display
 
 In order to display proof goals and information at point, `coq-lsp` supports the `proof/goals` request, parameters are:

fleche/doc.ml

@@ -145,7 +145,7 @@ module Diags : sig
 
   (** Build simple diagnostic *)
   val make :
-       ?data:Lang.Diagnostic.Data.t list
+       ?data:Lang.Diagnostic.Data.t
     -> Lang.Range.t
     -> Lang.Diagnostic.Severity.t
     -> Pp.t
@@ -175,17 +175,18 @@ end = struct
 
   (* ast-dependent error diagnostic generation *)
   let extra_diagnostics_of_ast stm_range ast =
-    let stm_range = Lang.Diagnostic.Data.SentenceRange stm_range in
-    match
-      Option.bind ast (fun (ast : Node.Ast.t) -> Coq.Ast.Require.extract ast.v)
-    with
-    | Some { Coq.Ast.Require.from; mods; _ } ->
-      let refs = List.map fst mods in
-      Some
-        [ stm_range
-        ; Lang.Diagnostic.Data.FailedRequire { prefix = from; refs }
-        ]
-    | _ -> Some [ stm_range ]
+    let sentenceRange = Some stm_range in
+    let failedRequire =
+      match
+        Option.bind ast (fun (ast : Node.Ast.t) ->
+            Coq.Ast.Require.extract ast.v)
+      with
+      | Some { Coq.Ast.Require.from; mods; _ } ->
+        let refs = List.map fst mods in
+        Some [ { Lang.Diagnostic.FailedRequire.prefix = from; refs } ]
+      | _ -> None
+    in
+    Some { Lang.Diagnostic.Data.sentenceRange; failedRequire }
 
   let extra_diagnostics_of_ast stm_range ast =
     if !Config.v.send_diags_extra_data then

lang/diagnostic.ml

@@ -4,13 +4,18 @@
 (* Written by: Emilio J. Gallego Arias                                  *)
 (************************************************************************)
 
+module FailedRequire = struct
+  type t =
+    { prefix : Libnames.qualid option
+    ; refs : Libnames.qualid list
+    }
+end
+
 module Data = struct
   type t =
-    | SentenceRange of Range.t
-    | FailedRequire of
-        { prefix : Libnames.qualid option
-        ; refs : Libnames.qualid list
-        }
+    { sentenceRange : Range.t option [@default None]
+    ; failedRequire : FailedRequire.t list option [@default None]
+    }
 end
 
 module Severity = struct
@@ -27,7 +32,7 @@ type t =
   { range : Range.t
   ; severity : Severity.t
   ; message : Pp.t
-  ; data : Data.t list option [@default None]
+  ; data : Data.t option [@default None]
   }
 
 let is_error { severity; _ } = severity = 1

lang/diagnostic.mli

@@ -4,13 +4,18 @@
 (* Written by: Emilio J. Gallego Arias                                  *)
 (************************************************************************)
 
+module FailedRequire : sig
+  type t =
+    { prefix : Libnames.qualid option
+    ; refs : Libnames.qualid list
+    }
+end
+
 module Data : sig
   type t =
-    | SentenceRange of Range.t
-    | FailedRequire of
-        { prefix : Libnames.qualid option
-        ; refs : Libnames.qualid list
-        }
+    { sentenceRange : Range.t option [@default None]
+    ; failedRequire : FailedRequire.t list option [@default None]
+    }
 end
 
 module Severity : sig
@@ -29,7 +34,7 @@ type t =
   { range : Range.t
   ; severity : Severity.t
   ; message : Pp.t
-  ; data : Data.t list option [@default None]
+  ; data : Data.t option [@default None]
   }
 
 val is_error : t -> bool

lsp/jLang.ml

@@ -37,9 +37,14 @@ end
 module Diagnostic = struct
   module Libnames = Serlib.Ser_libnames
 
+  module FailedRequire = struct
+    type t = [%import: Lang.Diagnostic.FailedRequire.t] [@@deriving yojson]
+  end
+
   module Data = struct
     module Lang = struct
       module Range = Range
+      module FailedRequire = FailedRequire
       module Diagnostic = Lang.Diagnostic
     end
 
@@ -78,7 +83,7 @@ module Diagnostic = struct
     { range : Range.t
     ; severity : int
     ; message : string
-    ; data : Data.t list option [@default None]
+    ; data : Data.t option [@default None]
     }
   [@@deriving yojson]