package coq-lsp

  1. Overview
  2. Docs
Language Server Protocol native server for Coq

Install

dune-project
 Dependency

Authors

Maintainers

Sources

coq-lsp-0.2.4.9.1.tbz
sha256=667908bdd88f0bb1b75d2fa76a483006d600c9422a2a15297a172e62c0415cad
sha512=42f8e5ad308702f77c9dc40243acd2e656b16bdb94c302306dbb87387cc36941deccd5f52c18d1a045467030ddf86528b22819522a647eee5b9e1ac25f4a9560

doc/coq-lsp.lsp/Fleche_lsp/Base/index.html

Module Fleche_lsp.BaseSource

Sourcemodule Params : sig ... end
Sourcemodule Notification : sig ... end
Sourcemodule Request : sig ... end
Sourcemodule Response : sig ... end
Sourcemodule Message : sig ... end

Basic JSON-RPC Incoming Messages

Build request

Sourcemodule ProgressToken : sig ... end

Progress

Sourcemodule ProgressParams : sig ... end
Sourceval mk_progress : token:ProgressToken.t -> value:'a -> ('a -> Yojson.Safe.t) -> Yojson.Safe.t
Sourcemodule WorkDoneProgressBegin : sig ... end
Sourcemodule WorkDoneProgressReport : sig ... end
Sourcemodule WorkDoneProgressEnd : sig ... end
Sourcemodule MessageParams : sig ... end
Sourceval mk_logMessage_ : type_:int -> message:string -> Notification.t

Create a logMessage LSP notification

Sourceval mk_logMessage : lvl:Fleche.Io.Level.t -> message:string -> Notification.t
Sourcemodule TraceParams : sig ... end
Sourceval mk_logTrace : message:string -> verbose:string option -> Notification.t

Create a logTrace notification