diff options
| author |  Carst Tankink <carst.tankink@inria.fr> | 2014-08-01 11:45:13 +0200 |
|---|---|---|
| committer |  Enrico Tassi <gares@fettunta.org> | 2014-08-04 16:13:59 +0200 |
| commit | 188b47917ed7de53fe5c37a39c8463a804fae038 (patch) | |
| tree | 142b33b2e759f51d69528d060ee386c5aae585ce /stm/stm.mli | |
| parent | b44eaad7da9787762ab51e3a3cee985805c862e4 (diff) | |
STM: VtQuery holds the id of the state it refers to
Diffstat (limited to 'stm/stm.mli')
| -rw-r--r-- | stm/stm.mli | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/stm/stm.mli b/stm/stm.mli index d36fd1571..3bc458f57 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -22,9 +22,10 @@ val add : ontop:Stateid.t -> ?newtip:Stateid.t -> ?check:(located_vernac_expr -> bool -> edit_id -> string -> Stateid.t * [ `NewTip | `Unfocus of Stateid.t ] -(* parses and xecutes a command at a given state, throws away its side effects - but for the printings *) -val query : at:Stateid.t -> string -> unit +(* parses and executes a command at a given state, throws away its side effects + but for the printings. Feedback is sent with report_with (defaults to dummy + state id) *) +val query : at:Stateid.t -> ?report_with:Stateid.t -> string -> 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 |