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

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.4.8.20.tbz
sha256=9e3736371fe2c2dd5af50e2a360f070f8c329516c60f01ba3dc7378b80b77172
sha512=d5302f5dc4d7700910b7a7a2d1558770e15bfc0c7bcf9de2ccfd321b4e3cd591848d8e11f03e87362a8d81df72ec4af57dda2c3c5737b34726dcee35de2e56c8

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;
}
Sourceval make : ?range:'l -> ?quickFix:'l Lang.Qf.t list -> Pp.t -> 'l t
Sourceval map : f:('l -> 'm) -> 'l t -> 'm t