diff options
Diffstat (limited to 'stm/stm.mli')
| -rw-r--r-- | stm/stm.mli | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/stm/stm.mli b/stm/stm.mli index 35ce77a3..1e5ceb7e 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -92,11 +92,11 @@ val new_doc : stm_init_options -> doc * Stateid.t (** [parse_sentence sid pa] Reads a sentence from [pa] with parsing state [sid] Returns [End_of_input] if the stream ends *) -val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Gram.coq_parsable -> +val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Parsable.t -> Vernacexpr.vernac_control CAst.t (* Reminder: A parsable [pa] is constructed using - [Pcoq.Gram.coq_parsable stream], where [stream : char Stream.t]. *) + [Pcoq.Parsable.t stream], where [stream : char Stream.t]. *) exception End_of_input @@ -110,11 +110,16 @@ val add : doc:doc -> ontop:Stateid.t -> ?newtip:Stateid.t -> bool -> Vernacexpr.vernac_control CAst.t -> doc * Stateid.t * [ `NewTip | `Unfocus of Stateid.t ] +(* Returns the proof state before the last tactic that was applied at or before +the specified state AND that has differences in the underlying proof (i.e., +ignoring proofview-only changes). Used to compute proof diffs. *) +val get_prev_proof : doc:doc -> Stateid.t -> Proof.t option + (* [query at ?report_with cmd] Executes [cmd] at a given state [at], throwing away side effects except messages. Feedback will be sent with [report_with], which defaults to the dummy state id *) val query : doc:doc -> - at:Stateid.t -> route:Feedback.route_id -> Pcoq.Gram.coq_parsable -> unit + at:Stateid.t -> route:Feedback.route_id -> Pcoq.Parsable.t -> unit (* [edit_at id] is issued to change the editing zone. [`NewTip] is returned if the requested id is the new document tip hence the document portion following @@ -263,11 +268,12 @@ val register_proof_block_delimiter : * the alternative toploop for the worker can be selected by changing * the name of the Task(s) above) *) -val state_computed_hook : (Stateid.t -> in_cache:bool -> unit) Hook.t -val unreachable_state_hook : (Stateid.t -> Exninfo.iexn -> unit) Hook.t +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 (* ready means that master has it at hand *) -val state_ready_hook : (Stateid.t -> unit) Hook.t +val state_ready_hook : (doc:doc -> Stateid.t -> unit) Hook.t (* Messages from the workers to the master *) val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t |