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.9.0.tbz
sha256=b6bf58331589b0bc750c01cc96a607322cf20260e61bd74f64998e04a9b909d3
sha512=b74f88117a180b089f99dc2d0cd867bdeb7aef071fa487334cdd2961ac61b9ba592e7f58c509dd6920ca2708dcc64992944009d4dce504bb5d0e28bb7d963c07

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