module Node : sig ... endmodule Completion : sig ... endtype 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.
val asts : t -> Node.Ast.t listReturn the list of all asts in the doc
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.tNote, create calls Coq but it is not cached in the Memo.t table
val bump_version : version:int -> raw:string -> t -> t Contents.R.tUpdate the contents of a document, updating the right structures for incremental checking.
module Target : sig ... endChecking targets, this specifies what we expect check to reach
val check : ofmt:Format.formatter -> target:Target.t -> doc:t -> unit -> tcheck ~ofmt ~target ~doc (), target will have Flèche stop after the point specified there has been reached.
val create_failed_permanent :
state:Coq.State.t ->
uri:Lang.LUri.File.t ->
version:int ->
raw:string ->
t Contents.R.tThis is internal, to workaround the Coq multiple-docs problem