[diagnostics] Add sentence's range to errors extra data field.

- We change diagnostics `extra` field to `data`, so we now conform to
  the LSP spec
- we include the data only when the `send_diags_extra_data`
  server-side option is enabled
- we now include range of full sentence in error diagnostic extra data

Thanks to @driverag22 for the idea, cc #663

CHANGES.md

@@ -67,6 +67,11 @@
    #513)
  - allow more than one input position in `selectionRange` LSP call
    (@ejgallego, #667, fixes #663)
+ - change diagnostic `extra` field to `data`, so we now conform to the
+   LSP spec, include the data only when the `send_diags_extra_data`
+   server-side option is enabled (@ejgallego, #670)
+ - include range of full sentence in error diagnostic extra data
+   (@ejgallego, #670 , thanks to @driverag22 for the idea, cc #663.
 
 # coq-lsp 0.1.8.1: Spring fix
 -----------------------------

editor/code/package.json

@@ -157,6 +157,11 @@
             "type": "number",
             "default": 150,
             "description": "Maximum number of errors per file, after that, coq-lsp will stop checking the file."
+          },
+          "coq-lsp.send_diags_extra_data": {
+            "type": "boolean",
+            "default": false,
+            "description": "Send extra diagnostics data, usually on error"
           }
         }
       },

etc/doc/PROTOCOL.md

@@ -72,6 +72,18 @@ to determine the content type. Supported extensions are:
 As of today, `coq-lsp` implements two extensions to the LSP spec. Note
 that none of them are stable yet:
 
+### Extra diagnostics data
+
+This is enabled if the server-side option `send_diags_extra_data` is
+set to `true`. In this case, some diagnostics may come with extra data
+in the optional `data` field.
+
+This field is experimental, and it can change without warning. As of
+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.
+
 ### Goal Display
 
 In order to display proof goals and information at point, `coq-lsp` supports the `proof/goals` request, parameters are:

fleche/config.ml

@@ -49,6 +49,9 @@ type t =
         (** Verbosity, 1 = reduced, 2 = default. As of today reduced will
             disable all logging, and the diagnostics and perf_data notification *)
   ; check_only_on_request : bool [@default false]
+        (** Experimental setting to check document lazily *)
+  ; send_diags_extra_data : bool [@default false]
+        (** Send extra diagnostic data on the `data` diagnostic field. *)
   }
 
 let default =
@@ -71,6 +74,7 @@ let default =
   ; send_perf_data = true
   ; send_diags = true
   ; check_only_on_request = false
+  ; send_diags_extra_data = false
   }
 
 let v = ref default

fleche/doc.ml

@@ -132,15 +132,19 @@ module Diags : sig
 
   (** Build simple diagnostic *)
   val make :
-       ?extra:Lang.Diagnostic.Extra.t list
+       ?data:Lang.Diagnostic.Data.t list
     -> Lang.Range.t
     -> Lang.Diagnostic.Severity.t
     -> Pp.t
     -> Lang.Diagnostic.t
 
   (** Build advanced diagnostic with AST analysis *)
   val error :
-    range:Lang.Range.t -> msg:Pp.t -> ast:Node.Ast.t -> Lang.Diagnostic.t
+       lines:string array
+    -> range:Lang.Range.t
+    -> msg:Pp.t
+    -> ast:Node.Ast.t
+    -> Lang.Diagnostic.t
 
   (** [of_messages drange msgs] process feedback messages, and convert some to
       diagnostics based on user-config. Default range [drange] is used for
@@ -152,20 +156,30 @@ module Diags : sig
 end = struct
   let err = Lang.Diagnostic.Severity.error
 
-  let make ?extra range severity message =
-    Lang.Diagnostic.{ range; severity; message; extra }
+  let make ?data range severity message =
+    Lang.Diagnostic.{ range; severity; message; data }
 
   (* ast-dependent error diagnostic generation *)
-  let extra_diagnostics_of_ast ast =
+  let extra_diagnostics_of_ast ~lines ast =
+    let stm_range = ast.Node.Ast.v |> Coq.Ast.loc |> Option.get in
+    let stm_range = Coq.Utils.to_range ~lines stm_range in
+    let stm_range = Lang.Diagnostic.Data.SentenceRange stm_range in
     match Coq.Ast.Require.extract ast.Node.Ast.v with
     | Some { Coq.Ast.Require.from; mods; _ } ->
       let refs = List.map fst mods in
-      Some [ Lang.Diagnostic.Extra.FailedRequire { prefix = from; refs } ]
-    | _ -> None
+      Some
+        [ stm_range
+        ; Lang.Diagnostic.Data.FailedRequire { prefix = from; refs }
+        ]
+    | _ -> Some [ stm_range ]
+
+  let extra_diagnostics_of_ast ~lines ast =
+    if !Config.v.send_diags_extra_data then extra_diagnostics_of_ast ~lines ast
+    else None
 
-  let error ~range ~msg ~ast =
-    let extra = extra_diagnostics_of_ast ast in
-    make ?extra range Lang.Diagnostic.Severity.error msg
+  let error ~lines ~range ~msg ~ast =
+    let data = extra_diagnostics_of_ast ~lines ast in
+    make ?data range Lang.Diagnostic.Severity.error msg
 
   let of_feed ~drange (range, severity, message) =
     let range = Option.default drange range in
@@ -736,7 +750,7 @@ let strategy_of_coq_err ~node ~state ~last_tok = function
   | Coq.Protect.Error.Anomaly _ -> Stop (Failed last_tok, node)
   | User _ -> Continue { state; last_tok; node }
 
-let node_of_coq_result ~token ~doc ~range ~ast ~st ~parsing_diags
+let node_of_coq_result ~lines ~token ~doc ~range ~ast ~st ~parsing_diags
     ~parsing_feedback ~feedback ~info last_tok res =
   match res with
   | Ok state ->
@@ -748,7 +762,7 @@ let node_of_coq_result ~token ~doc ~range ~ast ~st ~parsing_diags
   | Error (Coq.Protect.Error.Anomaly (err_range, msg) as coq_err)
   | Error (User (err_range, msg) as coq_err) ->
     let err_range = Option.default range err_range in
-    let err_diags = [ Diags.error ~range:err_range ~msg ~ast ] in
+    let err_diags = [ Diags.error ~lines ~range:err_range ~msg ~ast ] in
     let contents, nodes = (doc.contents, doc.nodes) in
     let context =
       Recovery_context.make ~contents ~last_tok ~nodes ~ast:ast.v ()
@@ -805,8 +819,8 @@ let document_action ~token ~st ~parsing_diags ~parsing_feedback ~parsing_time
          this point then, hence the new last valid token last_tok_new *)
       let last_tok_new = Coq.Parsing.Parsable.loc doc_handle in
       let last_tok_new = Coq.Utils.to_range ~lines last_tok_new in
-      node_of_coq_result ~token ~doc ~range:ast_range ~ast ~st ~parsing_diags
-        ~parsing_feedback ~feedback ~info last_tok_new res)
+      node_of_coq_result ~lines ~token ~doc ~range:ast_range ~ast ~st
+        ~parsing_diags ~parsing_feedback ~feedback ~info last_tok_new res)
 
 module Target = struct
   type t =

lang/diagnostic.ml

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

lang/diagnostic.mli

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

lsp/jLang.ml

@@ -37,6 +37,15 @@ end
 module Diagnostic = struct
   module Libnames = Serlib.Ser_libnames
 
+  module Data = struct
+    module Lang = struct
+      module Range = Range
+      module Diagnostic = Lang.Diagnostic
+    end
+
+    type t = [%import: Lang.Diagnostic.Data.t] [@@deriving yojson]
+  end
+
   (* LSP Ranges, a bit different from Fleche's ranges as points don't include
      offsets *)
   module Point = struct
@@ -69,14 +78,15 @@ module Diagnostic = struct
     { range : Range.t
     ; severity : int
     ; message : string
+    ; data : Data.t list option [@default None]
     }
   [@@deriving yojson]
 
-  let to_yojson { Lang.Diagnostic.range; severity; message; extra = _ } =
+  let to_yojson { Lang.Diagnostic.range; severity; message; data } =
     let range = Range.conv range in
     let severity = Lang.Diagnostic.Severity.to_int severity in
     let message = Pp.to_string message in
-    _t_to_yojson { range; severity; message }
+    _t_to_yojson { range; severity; message; data }
 end
 
 let mk_diagnostics ~uri ~version ld : Yojson.Safe.t =