Module Fleche.TheorySource

Sourcemodule Check : sig ... end
Sourceval open_ : io:Io.CallBack.t -> token:Coq.Limits.Token.t -> env:Doc.Env.t -> uri:Lang.LUri.File.t -> languageId:string -> raw:string -> version:int -> unit

Open a document inside a theory

Sourceval change : io:Io.CallBack.t -> token:Coq.Limits.Token.t -> uri:Lang.LUri.File.t -> version:int -> raw:string -> IS.t

Update a document inside a theory, returns the set of invalidated requests

Sourceval workspace_update : unit -> IS.t

Notify the theory manager that the workspace has changed, for example due to new .vo files present or updated. Returns the set of invalidated requests

Sourceval close : uri:Lang.LUri.File.t -> unit

Close a document

Sourcemodule Request : sig ... end
Sourcemodule Register : sig ... end