diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-02-16 14:14:34 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-12 16:18:08 +0200 |
| commit | 3a7d9fcafedc4987d0748a8717b2b012a779de39 (patch) | |
| tree | 59bded0fc995c7a9137f909832592a9c8ee8807f /stm/stm.mli | |
| parent | b209cea412a9541fd1c434dde36ea6eb1e256a33 (diff) | |
[stm] Remove edit_id.
We remove `edit_id` from the STM. In PIDE they serve a different
purpose, however in Coq they were of limited utility and required many
special cases all around the code.
Indeed, parsing is not an asynchronous operation in Coq, thus having
feedback about parsing didn't make much sense. All clients indeed
ignore such feedback and handle parsing in a synchronous way.
XML protocol clients are unaffected, they rely on the instead on the
Fail value.
This commit supersedes PR#203.
Diffstat (limited to 'stm/stm.mli')
| -rw-r--r-- | stm/stm.mli | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/stm/stm.mli b/stm/stm.mli index a89062c29..d3e5dde39 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -13,8 +13,8 @@ open Loc (** state-transaction-machine interface *) -(* [add ontop check vebose eid s] adds a new command [s] on the state [ontop] - having edit id [eid]. [check] is called on the AST. +(* [add ontop check vebose eid s] adds a new command [s] on the state [ontop]. + [check] is called on the AST. The [ontop] parameter is just for asserting the GUI is on sync, but will eventually call edit_at on the fly if needed. The sentence [s] is parsed in the state [ontop]. @@ -23,7 +23,7 @@ open Loc val add : ontop:Stateid.t -> ?newtip:Stateid.t -> ?check:(vernac_expr located -> unit) -> - bool -> edit_id -> string -> + bool -> string -> Stateid.t * [ `NewTip | `Unfocus of Stateid.t ] (* parses and executes a command at a given state, throws away its side effects @@ -182,9 +182,8 @@ val register_proof_block_delimiter : * the name of the Task(s) above) *) 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 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 |