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 (38)

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+8.20.tbz
sha256=764f5cbaf3da308a21ea2953a275e74b6e5a841c82bdd8b71fa474b1395738a1
sha512=16189385a27ce7576820d03d4410d4f9bc52150b43d714813c3611d6b5519b5d256c1ac348913bbf77c6f313d54927ead935a188783e04b21032f5e06c793778

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