Module `Stm`

module AsyncOpts : sig ... end

type interactive_top = | TopLogical of Names.DirPath.t | TopPhysical of string
type stm_doc_type = | VoDoc of string | VioDoc of string | Interactive of interactive_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 option_command = | OptionSet of string option | OptionUnset
type injection_command = | OptionInjection of Goptions.option_name * option_command Set flags or options before the initial state is ready. | RequireInjection of string * string option * bool option Require libraries before the initial state is ready. Parameters follow Library, that is to say, lib,prefix,import_export means require library lib from optional prefix and import_export if Some false/Some true is used.
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. ml_load_path : CUnix.physical_path list; OCaml load paths for the document. vo_load_path : Loadpath.vo_path list; vo load paths for the document. Usually extracted from -R options / _CoqProject injections : injection_command list; Injects Require and Set/Unset commands before the initial state is ready stm_options : AsyncOpts.stm_opt; Low-level STM options }: STM initialization options:

val init_core : unit -> unit: init_core performs some low-level initialization; should go away in future releases.

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 add : doc:doc -> ontop:Stateid.t -> ?⁠newtip:Stateid.t -> bool -> Vernacexpr.vernac_control -> doc * Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
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; }

val edit_at : doc:doc -> Stateid.t -> doc * [ `NewTip | `Focus of focus ]
val observe : doc:doc -> Stateid.t -> doc
val finish : doc:doc -> doc
val wait : doc:doc -> doc
val stop_worker : string -> unit
val join : doc:doc -> doc
val snapshot_vio : create_vos:bool -> doc:doc -> output_native_objects:bool -> Names.DirPath.t -> string -> doc
val reset_task_queue : unit -> unit

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 : Goal.goal list; recovery_command : Vernacexpr.vernac_control option; }
type dynamic_block_error_recovery = doc -> static_block_declaration -> [ `ValidBlock of recovery_action | `Leaks ]

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) Hook.t
val unreachable_state_hook : (doc:doc -> Stateid.t -> Exninfo.iexn -> unit) Hook.t
val state_ready_hook : (doc:doc -> Stateid.t -> unit) Hook.t
val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t
val document_add_hook : (Vernacexpr.vernac_control -> Stateid.t -> unit) Hook.t: User adds a sentence to the document (after parsing)

val document_edit_hook : (Stateid.t -> unit) Hook.t: User edits a sentence in the document

val sentence_exec_hook : (Stateid.t -> unit) Hook.t: User requests evaluation of a sentence

val get_doc : Feedback.doc_id -> doc
val state_of_id : doc:doc -> Stateid.t -> [ `Valid of Vernacstate.t option | `Expired | `Error of exn ]
val current_proof_depth : doc:doc -> int
val get_all_proof_names : doc:doc -> Names.Id.t list
val stm_debug : bool Stdlib.ref: Enable STM debugging

`\|` `OptionInjection of Goptions.option_name * option_command`	Set flags or options before the initial state is ready.
`\|` `RequireInjection of string * string option * bool option`	Require libraries before the initial state is ready. Parameters follow `Library`, that is to say, `lib,prefix,import_export` means require library `lib` from optional `prefix` and `import_export` if `Some false/Some true` is used.

`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.
`ml_load_path : CUnix.physical_path list;`	OCaml load paths for the document.
`vo_load_path : Loadpath.vo_path list;`	`vo` load paths for the document. Usually extracted from -R options / _CoqProject
`injections : injection_command list;`	Injects Require and Set/Unset commands before the initial state is ready
`stm_options : AsyncOpts.stm_opt;`	Low-level STM options