1 files changed, 12 insertions, 5 deletions
diff --git a/stm/stm.mli b/stm/stm.mli
index 1d926e99..0c05c93d 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -35,7 +35,9 @@ val query :
    new document tip, the document between [id] and [fo.stop] has been dropped.
    The portion between [fo.stop] and [fo.tip] has been kept.  [fo.start] is
    just to tell the gui where the editing zone starts, in case it wants to
-   graphically denote it.  All subsequent [add] happen on top of [id]. *)
+   graphically denote it.  All subsequent [add] happen on top of [id].
+   If Flags.async_proofs_full is set, then [id] is not [observe]d, else it is.
+*)
 type focus = { start : Stateid.t; stop : Stateid.t; tip : Stateid.t }
 val edit_at : Stateid.t -> [ `NewTip | `Focus of focus ]
 
@@ -49,11 +51,11 @@ val stop_worker : string -> unit
 (* Joins the entire document.  Implies finish, but also checks proofs *)
 val join : unit -> unit
 
-(* Saves on the dist a .vio corresponding to the current status:
-   - if the worker prool is empty, all tasks are saved
+(* Saves on the disk a .vio corresponding to the current status:
+   - if the worker pool is empty, all tasks are saved
    - if the worker proof is not empty, then it waits until all workers
      are done with their current jobs and then dumps (or fails if one
-     of the completed tasks is a failuere) *)
+     of the completed tasks is a failure) *)
 val snapshot_vio : DirPath.t -> string -> unit
 
 (* Empties the task queue, can be used only if the worker pool is empty (E.g.
@@ -81,6 +83,10 @@ val set_compilation_hints : string -> unit
 (* Reorders the task queue putting forward what is in the perspective *)
 val set_perspective : Stateid.t list -> unit
 
+type document
+val backup : unit -> document
+val restore : document -> unit
+
 (** workers **************************************************************** **)
 
 module ProofTask : AsyncTaskQueue.Task
@@ -98,7 +104,7 @@ val state_computed_hook : (Stateid.t -> in_cache:bool -> unit) Hook.t
 val parse_error_hook :
   (Feedback.edit_or_state_id -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t
 val execution_error_hook : (Stateid.t -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t
-val unreachable_state_hook : (Stateid.t -> unit) Hook.t
+val unreachable_state_hook : (Stateid.t -> Exninfo.iexn -> unit) Hook.t
 (* ready means that master has it at hand *)
 val state_ready_hook : (Stateid.t -> unit) Hook.t
 
@@ -130,3 +136,4 @@ val process_error_hook : Future.fix_exn Hook.t
 val interp_hook : (?verbosely:bool -> ?proof:Proof_global.closed_proof ->
   Loc.t * Vernacexpr.vernac_expr -> unit) Hook.t
 val with_fail_hook : (bool -> (unit -> unit) -> unit) Hook.t
+val get_fix_exn : unit -> (Exninfo.iexn -> Exninfo.iexn)