Stm
state-transaction-machine interface
module AsyncOpts : sig ... end
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 |
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 options opt
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 from pa
with parsing state sid
and non terminal entry
. 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).
val query :
doc:doc ->
at:Stateid.t ->
route:Feedback.route_id ->
Pcoq.Parsable.t ->
unit
val edit_at : doc:doc -> Stateid.t -> doc * edit_focus
val finish : doc:doc -> Vernacstate.t
val wait : doc:doc -> unit
val join : doc:doc -> unit
val snapshot_vio :
create_vos:bool ->
doc:doc ->
output_native_objects:bool ->
Names.DirPath.t ->
string ->
unit
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_ldir : doc:doc -> Names.DirPath.t
val get_ast : doc:doc -> Stateid.t -> Vernacexpr.vernac_control option
workers **************************************************************** *
module ProofTask : AsyncTaskQueue.Task
module QueryTask : AsyncTaskQueue.Task
document structure customization *************************************** *
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_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 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
customization ********************************************************** *
val unreachable_state_hook :
( doc:doc -> Stateid.t -> Exninfo.iexn -> 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
val current_proof_depth : doc:doc -> int
val get_all_proof_names : doc:doc -> Names.Id.t list
val backup : unit -> document
val restore : document -> unit