diff --git a/CHANGES.md b/CHANGES.md index de4884e10..93b4e5603 100644 --- a/CHANGES.md +++ b/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 ----------------------------------- diff --git a/etc/doc/PROTOCOL.md b/etc/doc/PROTOCOL.md index a9d3322b7..6b167e774 100644 --- a/etc/doc/PROTOCOL.md +++ b/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: diff --git a/fleche/doc.ml b/fleche/doc.ml index fbde2b1ef..4c02c7b2e 100644 --- a/fleche/doc.ml +++ b/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 diff --git a/lang/diagnostic.ml b/lang/diagnostic.ml index 393b1168c..84b307536 100644 --- a/lang/diagnostic.ml +++ b/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 diff --git a/lang/diagnostic.mli b/lang/diagnostic.mli index 220d85470..282d10f6d 100644 --- a/lang/diagnostic.mli +++ b/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 diff --git a/lsp/jLang.ml b/lsp/jLang.ml index e54907036..27e17c045 100644 --- a/lsp/jLang.ml +++ b/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]