diff options
| author | Emilio Jesus Gallego Arias | 2017-02-16 14:14:34 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-04-12 16:18:08 +0200 |
| commit | 3a7d9fcafedc4987d0748a8717b2b012a779de39 (patch) | |
| tree | 59bded0fc995c7a9137f909832592a9c8ee8807f /ide/interface.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 'ide/interface.mli')
| -rw-r--r-- | ide/interface.mli | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/ide/interface.mli b/ide/interface.mli index 9ed6062588..62f63aefb9 100644 --- a/ide/interface.mli +++ b/ide/interface.mli @@ -111,8 +111,10 @@ type coq_info = { (** Calls result *) type location = (int * int) option (* start and end of the error *) -type state_id = Feedback.state_id -type edit_id = Feedback.edit_id +type state_id = Stateid.t + +(* Obsolete *) +type edit_id = int (* The fail case carries the current state_id of the prover, the GUI should probably retract to that point *) |