Module Fleche.DocSource

Sourcemodule Node : sig ... end
Sourcemodule Completion : sig ... end
Sourcetype t = private {
  1. uri : string;
  2. version : int;
  3. contents : string;
  4. end_loc : Types.Point.t;
  5. root : Coq.State.t;
  6. nodes : Node.t list;
  7. diags_dirty : bool;
  8. completed : Completion.t;
  9. stats : Stats.t;
    (*

    Info about cumulative document stats

    *)
}

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 create : state:Coq.State.t -> workspace:Coq.Workspace.t -> uri:string -> version:int -> contents:string -> 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 ~fb_queue ?cutpoint ~doc if set, cutpoint will have Flèche stop after the point specified there has been reached.