package coq-lsp

  1. Overview
  2. Docs
module Node : sig ... end
module Contents : sig ... end
module Completion : sig ... end
type t = private {
  1. uri : string;
  2. version : int;
  3. contents : Contents.t;
  4. root : Coq.State.t;
  5. nodes : Node.t list;
  6. diags_dirty : bool;
  7. 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.

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

Return the list of all asts in the doc

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

val bump_version : version:int -> contents:string -> t -> t

Update the contents of a document, updating the right structures for incremental checking.

module Target : sig ... end

Checking targets, this specifies what we expect check to reach

val 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.