diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-09-30 22:18:56 +0200 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-10-08 09:51:13 +0200 |
commit | f7e9e6428842dd80549a0dcd20bf872c2dd7fa8c (patch) | |
tree | 1065eccd48e1c291faec73dcf75ee9777adfcab5 /stm/stm.mli | |
parent | 173f07a8386bf4d3d45b49d3dc01ab047b3ad4f9 (diff) |
STM: for PIDE based UIs, edit_at requires no Reach.known_state
Diffstat (limited to 'stm/stm.mli')
-rw-r--r-- | stm/stm.mli | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/stm/stm.mli b/stm/stm.mli index 1d926e998..4bad7f0a6 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. |