diff --git a/CHANGES.md b/CHANGES.md index de4884e1..93b4e560 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 a9d3322b..6b167e77 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 fbde2b1e..4c02c7b2 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 393b1168..84b30753 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 220d8547..282d10f6 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 e5490703..27e17c04 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]