package coq-lsp
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=bcb9a4c3219aed47ffbfd7c8ea7a2f374140d8cdb76079927548f49c7e3576a9
sha512=945c0010b4952e41055cb7e35175d400e5c126dc340dd1c0ab53321605cd0d9539af6693a794cb81a9dec0385d0880d4417dae923b6d19c9b62913766a185d8c
doc/coq-lsp.fleche/Fleche/Doc/index.html
Module Fleche.DocSource
Enviroment external to the document, this includes for now the init Coq state and the workspace, which are used to build the first state of the document, usually by importing the prelude and other libs implicitly.
type t = private {uri : Lang.LUri.File.t;(*
*)uriof the documentversion : int;(*
*)versionof the documentcontents : Contents.t;(*
*)contentsof the documentnodes : Node.t list;(*List of document nodes
*)completed : Completion.t;(*Status of the document, usually either completed, suspended, or waiting for some IO / external event
*)toc : Node.t CString.Map.t;(*table of contents
*)env : Env.t;(*External document enviroment
*)root : Coq.State.t;(*
*)rootcontains the first state document state, obtained by applying a workspace to Coq's initial statediags_dirty : bool;(*internal field
*)
}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.
Return the list of all asts in the doc
Return the list of all diags in the doc
val create :
token:Coq.Limits.Token.t ->
env:Env.t ->
uri:Lang.LUri.File.t ->
version:int ->
raw:string ->
tCreate a new Coq document, this is cached! Note that this operation always suceeds, but the document could be created in a `Failed` state if problems arise.
Update the contents of a document, updating the right structures for incremental checking. If the operation fails, the document will be left in `Failed` state.
val check :
io:Io.CallBack.t ->
token:Coq.Limits.Token.t ->
target:Target.t ->
doc:t ->
unit ->
tcheck ~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.
save ~doc will save doc .vo file. It will fail if proofs are open, or if the document completion status is not Yes