Module Stm
module AsyncOpts : sig ... end
type stm_doc_type
=
|
VoDoc of string
|
VioDoc of string
|
Interactive of Coqargs.top
The STM document type
stm_doc_type
determines some properties such as what uncompleted proofs are allowed and what gets recorded to aux files.
type stm_init_options
=
{
doc_type : stm_doc_type;
The STM does set some internal flags differently depending on the specified
doc_type
. This distinction should disappear at some some point.injections : Coqargs.injection_command list;
Injects Require and Set/Unset commands before the initial state is ready
}
STM initialization options:
val init_process : AsyncOpts.stm_opt -> unit
init_process
performs some low-level initialization, call early
val new_doc : stm_init_options -> doc * Stateid.t
new_doc opt
Creates a new document with optionsopt
val parse_sentence : doc:doc -> Stateid.t -> entry:(Pvernac.proof_mode option -> 'a Pcoq.Entry.t) -> Pcoq.Parsable.t -> 'a
parse_sentence sid entry pa
Reads a sentence frompa
with parsing statesid
and non terminalentry
.entry
receives in input the current proof mode.sid
should be associated with a valid parsing state (which may not be the case if an error was raised at parsing time).
type add_focus
=
|
NewAddTip
|
Unfocus of Stateid.t
val add : doc:doc -> ontop:Stateid.t -> ?newtip:Stateid.t -> bool -> Vernacexpr.vernac_control -> doc * Stateid.t * add_focus
val get_prev_proof : doc:doc -> Stateid.t -> Proof.t option
val get_proof : doc:doc -> Stateid.t -> Proof.t option
val query : doc:doc -> at:Stateid.t -> route:Feedback.route_id -> Pcoq.Parsable.t -> unit
type focus
=
{
start : Stateid.t;
stop : Stateid.t;
tip : Stateid.t;
}
type edit_focus
=
|
NewTip
|
Focus of focus
val edit_at : doc:doc -> Stateid.t -> doc * edit_focus
val observe : doc:doc -> Stateid.t -> unit
val finish : doc:doc -> Vernacstate.t
val wait : doc:doc -> unit
val stop_worker : string -> unit
val join : doc:doc -> unit
val snapshot_vio : create_vos:bool -> doc:doc -> output_native_objects:bool -> Names.DirPath.t -> string -> unit
val reset_task_queue : unit -> unit
type document
type tasks
= (Opaqueproof.opaque_handle option, document) Library.tasks
val check_task : string -> tasks -> int -> bool
val info_tasks : tasks -> (string * float * int) list
val finish_tasks : string -> Library.seg_univ -> Library.seg_proofs -> tasks -> Library.seg_univ * Library.seg_proofs
val get_current_state : doc:doc -> Stateid.t
val get_ldir : doc:doc -> Names.DirPath.t
val get_ast : doc:doc -> Stateid.t -> Vernacexpr.vernac_control option
val set_compilation_hints : string -> unit
val set_perspective : doc:doc -> Stateid.t list -> unit
module ProofTask : AsyncTaskQueue.Task
module QueryTask : AsyncTaskQueue.Task
module DynBlockData : Dyn.S
type static_block_declaration
=
{
block_start : Stateid.t;
block_stop : Stateid.t;
dynamic_switch : Stateid.t;
carry_on_data : DynBlockData.t;
}
type document_node
=
{
indentation : int;
ast : Vernacexpr.vernac_control;
id : Stateid.t;
}
type document_view
=
{
entry_point : document_node;
prev_node : document_node -> document_node option;
}
type static_block_detection
= document_view -> static_block_declaration option
type recovery_action
=
{
base_state : Stateid.t;
goals_to_admit : Evar.t list;
recovery_command : Vernacexpr.vernac_control option;
}
type block_classification
=
|
ValidBlock of recovery_action
|
Leaks
type dynamic_block_error_recovery
= doc -> static_block_declaration -> block_classification
val register_proof_block_delimiter : Vernacextend.proof_block_name -> static_block_detection -> dynamic_block_error_recovery -> unit
val state_computed_hook : (doc:doc -> Stateid.t -> in_cache:bool -> unit) -> unit
val unreachable_state_hook : (doc:doc -> Stateid.t -> Exninfo.iexn -> unit) -> unit
val state_ready_hook : (doc:doc -> Stateid.t -> unit) -> unit
val forward_feedback_hook : (Feedback.feedback -> unit) -> unit
val document_add_hook : (Vernacexpr.vernac_control -> Stateid.t -> unit) -> unit
User adds a sentence to the document (after parsing)
val document_edit_hook : (Stateid.t -> unit) -> unit
User edits a sentence in the document
val sentence_exec_hook : (Stateid.t -> unit) -> unit
User requests evaluation of a sentence
val get_doc : Feedback.doc_id -> doc
type state
=
|
Valid of Vernacstate.t option
|
Expired
|
Error of exn