coq-lsp.lsp
Lsp.Core
Core LSP protocoal and language types
Astdump_plugin
Example_plugin
Goaldumpl_plugin
Savevo_plugin
coq-lsp.coq
coq-lsp.fleche
coq-lsp.lang
coq-lsp.petanque
coq-lsp.plugin
fleche_waterproof
petanque_json
module Location : sig ... end
module LocationLink : sig ... end
module DocumentSymbol : sig ... end
module SymInfo : sig ... end
Not used as of today, superseded by DocumentSymbol
module HoverContents : sig ... end
module HoverInfo : sig ... end
module LabelDetails : sig ... end
module TextEditReplace : sig ... end
module CompletionData : sig ... end
module Command : sig ... end
Code Lenses
module CodeLens : sig ... end
module SelectionRange : sig ... end
SelectionRange
module DocumentDiagnosticParams : sig ... end
Pull Diagnostics
module FullDocumentDiagnosticReport : sig ... end
module UnchangedDocumentDiagnosticReport : sig ... end
module DocumentDiagnosticReportPartialResult : sig ... end
partial result: The first literal send need to be a DocumentDiagnosticReport followed by n DocumentDiagnosticReportPartialResult literals defined as follows: