Module Fleche.DocSource

Sourcemodule Node : sig ... end
Sourcemodule Contents : sig ... end
Sourcemodule Completion : sig ... end
Sourcetype 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.

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

Return the list of all asts in the doc

Sourceval 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

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 ~target ~doc (), target will have Flèche stop after the point specified there has been reached.