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.4.v8.16.tbz

sha256=50df59eafc5b24a881c1a1dda6f6032b1da35b9b6ade7cb9e39968def9319508

sha512=e1d383b6802758cdbe5cbc6278af275d7951acd78224cdcfe622428942e84366ca283bf375d6e535ad7e8d8e847df84bd763bb2a263fc457dc5aead386c2836d

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

Module `Fleche.Doc`Source

Sourcemodule Node : sig ... end

Sourcemodule Contents : sig ... end

Sourcemodule Completion : sig ... end

Sourcetype t = private {

uri : string;
version : int;
contents : Contents.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 Loc.t -> data, where for now data is the contents of Node.t.

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

Return the list of all asts in the doc

Source

val create : 
  state:Coq.State.t ->
  workspace:Coq.Workspace.t ->
  uri:string ->
  version:int ->
  contents: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 -> contents:string -> t -> 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.