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.5.1.8.16.tbz
sha256=bd1d61581eed552aef1b2a37442684a9f96240f1faaf695330c33391a8742a4a
sha512=44566902af1ef750d901527b4b9f5ef9872cfed88a935fe94a78e5a07692855949fed5d71e6709a19f5bf619cf3640391f393fdfeaa98834e72c35106af460c3

doc/coq-lsp.fleche/Fleche/Doc/index.html

Module Fleche.DocSource

Sourcemodule Node : sig ... end
Sourcemodule Completion : sig ... end
Sourcetype t = private {
  1. uri : Lang.LUri.File.t;
  2. version : int;
  3. contents : Contents.t;
  4. toc : Lang.Range.t Coq.Ast.Id.Map.t;
  5. root : Coq.State.t;
  6. nodes : Node.t list;
  7. diags_dirty : bool;
  8. completed : Completion.t;
}

A Flèche document is basically a node list, which is a crude form of a meta-data map Range.t -> data, where for now data is the contents of Node.t.

Sourceval asts : t -> Node.Ast.t list

Return the list of all asts in the doc

Sourceval create : state:Coq.State.t -> workspace:Coq.Workspace.t -> uri:Lang.LUri.File.t -> version:int -> raw:string -> (t, Loc.t) Coq.Protect.R.t

Note, create calls Coq but it is not cached in the Memo.t table

Sourceval bump_version : version:int -> raw:string -> t -> t Contents.R.t

Update the contents of a document, updating the right structures for incremental checking.

Sourcemodule Target : sig ... end

Checking targets, this specifies what we expect check to reach

Sourceval check : ofmt:Format.formatter -> target:Target.t -> doc:t -> unit -> t

check ~ofmt ~target ~doc (), target will have Flèche stop after the point specified there has been reached.

Sourceval create_failed_permanent : state:Coq.State.t -> uri:Lang.LUri.File.t -> version:int -> raw:string -> t Contents.R.t

This is internal, to workaround the Coq multiple-docs problem