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

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.1.6.1.8.17.tbz
sha256=0b0ea3ce68aa549f61c004dd05d2b386dc18811ec4c9ac667ff2917857758707
sha512=d3e3ae7e055c1be38368fdc86679462e2aa4636805142e8fd1f73423a14a7c87e06d752f04964377fe39ed10972e3c47d433127694b104c0285adb976faadf66

doc/coq-lsp.lsp/Lsp/Io/index.html

Module Lsp.IoSource

JSON-RPC input/output

Sourceval read_raw_request : in_channel -> Yojson.Safe.t option

Read a JSON-RPC request from channel

Sourceval read_request : in_channel -> Base.Message.t option

None signals EOF

Sourceexception ReadError of string
Sourceval send_json : Format.formatter -> Yojson.Safe.t -> unit

Send a JSON-RPC request to channel

Logging

Sourcemodule TraceValue : sig ... end

Trace values

Sourceval set_trace_value : TraceValue.t -> unit

Set the trace value

Sourceval set_log_channel : Format.formatter -> unit

Set the log channel

Sourceval logMessage : lvl:int -> message:string -> unit

Send a window/logMessage notification to the client

Sourceval logTrace : message:string -> extra:string option -> unit

Send a $/logTrace notification to the client

Sourceval trace : string -> ?extra:string -> string -> unit

log hdr ?extra message Log message to server info log with header hdr. extra will be used when trace_value is set to Verbose

Sourceval trace_object : string -> Yojson.Safe.t -> unit

Log JSON object to server info log