package coq-lsp

You can search for identifiers within the package.

in-package search v0.2.0

Language Server Protocol native server for Coq

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (32)

Authors

Maintainers

E

e@x80.org

Sources

coq-lsp-0.1.8.8.18.tbz

sha256=0f6d12e00d145c36a17c5a6661bae83ae9e86b4cb09638d1d1a70f42abfdfdde

sha512=33200cfa5d9c44f8af7fd26fd4aca85a11b5639a73080a1f002993be1594cbbef6447aa6116a2c9527d2734d34c718c1adf51ee3aff1c8efbfb86d2cb4059335

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

Module `Fleche.Doc`Source

Sourcemodule Node : sig ... end

Sourcemodule Completion : sig ... end

Sourcetype t = private {

uri : Lang.LUri.File.t;
version : int;
contents : Contents.t;
toc : Lang.Range.t CString.Map.t;
root : Coq.State.t;
nodes : Node.t list;
diags_dirty : bool;
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 diags : t -> Lang.Diagnostic.t list

Return the list of all diags in the doc

Source

val 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

Create a new Coq document, this is cached!

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 : io:Io.CallBack.t -> target:Target.t -> doc:t -> unit -> t

check ~io ~target ~doc (), check document doc, target will have Flèche stop after the point specified there has been reached. Output functions are in the io record, used to send partial updates.

Sourceval save : doc:t -> (unit, Loc.t) Coq.Protect.E.t

save ~doc will save doc .vo file. It will fail if proofs are open, or if the document completion status is not Yes