Fleche.Doc
module Node : sig ... end
module Completion : sig ... end
module Env : sig ... end
Enviroment external to the document, this includes for now the init
Coq state and the workspace
, which are used to build the first state of the document, usually by importing the prelude and other libs implicitly.
type t = private {
uri : Lang.LUri.File.t;
uri
of the document
version : int;
version
of the document
contents : Contents.t;
contents
of the document
nodes : Node.t list;
List of document nodes
*)completed : Completion.t;
Status of the document, usually either completed, suspended, or waiting for some IO / external event
*)toc : Node.t CString.Map.t;
table of contents
*)env : Env.t;
External document enviroment
*)root : Coq.State.t;
root
contains the first state document state, obtained by applying a workspace to Coq's initial state
diags_dirty : bool;
internal field
*)}
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 list
Return the list of all asts in the doc
val diags : t -> Lang.Diagnostic.t list
Return the list of all diags in the doc
val create :
token:Coq.Limits.Token.t ->
env:Env.t ->
uri:Lang.LUri.File.t ->
version:int ->
raw:string ->
t
Create a new Coq document, this is cached! Note that this operation always suceeds, but the document could be created in a `Failed` state if problems arise.
val bump_version :
token:Coq.Limits.Token.t ->
version:int ->
raw:string ->
t ->
t
Update the contents of a document, updating the right structures for incremental checking. If the operation fails, the document will be left in `Failed` state.
module Target : sig ... end
Checking targets, this specifies what we expect check to reach
val check :
io:Io.CallBack.t ->
token:Coq.Limits.Token.t ->
target:Target.t ->
doc:t ->
unit ->
t
check ~io ~target ~doc ()
, check document doc
, target
will have Flèche stop after the point specified there has been reached. Output functions are in the io
record, used to send partial updates.
val save : token:Coq.Limits.Token.t -> doc:t -> (unit, Loc.t) Coq.Protect.E.t
save ~doc
will save doc
.vo file. It will fail if proofs are open, or if the document completion status is not Yes
val create_failed_permanent :
env:Env.t ->
uri:Lang.LUri.File.t ->
version:int ->
raw:string ->
t
This is internal, to workaround the Coq multiple-docs problem