package coq-lsp

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

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (36)

Authors

  1. E
    Emilio Jesús Gallego Arias <e@x80.org>
  2. A
    Ali Caglayan <alizter@gmail.com>
  3. S
    Shachar Itzhaky <shachari@cs.technion.ac.il>
  4. R
    Ramkumar Ramachandra <r@artagnon.com>

Maintainers

  1. E
    e@x80.org

Sources

coq-lsp-0.2.5+9.1.tbz
sha256=488520e2720cd0601a623be39ff87223d81ca1d2f81c77641f803fda21f3717e
sha512=146e43a6a9c516f4e7fe143d4fdf3e1e7ecdcd73ea5cc3e09b2886f68aa05210c016e905bf1596341faa0b55709ad530ef86212c92790b6dce6050a0a00e3325

doc/coq-lsp.coq/Coq/Message/Payload/index.html

Module Message.PayloadSource

Coq provides payload to our layer via two different mechanisms:

  • feedback messages
  • error exceptions

In both cases, the payload is the same, and it comes via different ways due to historical reasons. We abstract the payload as to better handle the common paths.

Sourcetype 'l t = {
  1. range : 'l option;
  2. quickFix : 'l Lang.Qf.t list option;
  3. msg : Pp_t.t;
}
Sourceval make : ?range:'l -> ?quickFix:'l Lang.Qf.t list -> Pp_t.t -> 'l t
Sourceval map : f:('l -> 'm) -> 'l t -> 'm t