package coq-lsp
Language Server Protocol native server for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
coq-lsp-0.1.5.1.8.16.tbz
sha256=bd1d61581eed552aef1b2a37442684a9f96240f1faaf695330c33391a8742a4a
sha512=44566902af1ef750d901527b4b9f5ef9872cfed88a935fe94a78e5a07692855949fed5d71e6709a19f5bf619cf3640391f393fdfeaa98834e72c35106af460c3
doc/coq-lsp.fleche/Fleche/Doc/index.html
Module Fleche.Doc
Source
Source
type t = private {
uri : Lang.LUri.File.t;
version : int;
contents : Contents.t;
toc : Lang.Range.t Coq.Ast.Id.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
.
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
Note, create
calls Coq but it is not cached in the Memo.t table
Update the contents of a document, updating the right structures for incremental checking.
check ~ofmt ~target ~doc ()
, target
will have Flèche stop after the point specified there has been reached.
Source
val create_failed_permanent :
state:Coq.State.t ->
uri:Lang.LUri.File.t ->
version:int ->
raw:string ->
t Contents.R.t
This is internal, to workaround the Coq multiple-docs problem
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>