diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-07-10 16:00:07 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-07-11 10:15:06 +0200 |
| commit | 8708cd63ee4604665d2f9eff0153931bd17c25bb (patch) | |
| tree | 2da1ad7d02e3b9077d7f7ddec5bc7162a53155c0 /stm/stm.mli | |
| parent | 2a805fd99b96746dbfe381d64cd7eaba84fdca79 (diff) | |
STM: export the observe function (useful for pide)
Diffstat (limited to 'stm/stm.mli')
| -rw-r--r-- | stm/stm.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/stm/stm.mli b/stm/stm.mli index fd306425c..e5327cb83 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -38,6 +38,8 @@ val edit_at : Stateid.t -> [ `NewTip | `Focus of focus ] (* Evaluates the tip of the current branch *) val finish : unit -> unit +val observe : Stateid.t -> unit + val stop_worker : int -> unit (* Joins the entire document. Implies finish, but also checks proofs *) |