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

sha256=d6d589ae18453d9251b4250df50e59cfc87254de0e4734e13c5bca06ab14cee5

sha512=802b4673c7f581976526a3cb4bd824f7574c5b1cc8fcc7759fcd3358cdc3e4cebef3ec908899ad68129190777ccda931dfc1643b45db156ede15acae0382c148

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

Module `Fleche.Doc`Source

Sourcemodule Node : sig ... end

Sourcemodule Completion : sig ... end

Sourcetype t = private {

uri : string;
version : int;
contents : string;
end_loc : Types.Point.t;
root : Coq.State.t;
nodes : Node.t list;
diags_dirty : bool;
completed : Completion.t;
stats : Stats.t;
(*
Info about cumulative document stats
*)

}

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.

Source

val create : 
  state:Coq.State.t ->
  workspace:Coq.Workspace.t ->
  uri:string ->
  version:int ->
  contents:string ->
  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 ~fb_queue ?cutpoint ~doc if set, cutpoint will have Flèche stop after the point specified there has been reached.