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.6.1.8.17.tbz

sha256=0b0ea3ce68aa549f61c004dd05d2b386dc18811ec4c9ac667ff2917857758707

sha512=d3e3ae7e055c1be38368fdc86679462e2aa4636805142e8fd1f73423a14a7c87e06d752f04964377fe39ed10972e3c47d433127694b104c0285adb976faadf66

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

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 : 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 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