diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-19 19:55:17 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-19 23:06:25 +0200 |
| commit | b3ed40b82540639de925afd36a32fbd716d2800f (patch) | |
| tree | 5c395650ce4495e4e4e6442cc5fd8a57ed4be60a /ide/document.mli | |
| parent | beb3acd2fd3831404f0be2da61d3f28e210e8349 (diff) | |
[ide] Rely less on `Stateid.dummy`
In particular, we set queries from the menu to the tip of the
document, and process feedback coming with a `dummy` id.
There are still more places to tweak, but this should be good for now.
We also display a few more query messages, in particular the feedbacks
produced by query that carry a dummy state id.
This hack of reporting with from the STM should be solved once we
update the protocol.
Diffstat (limited to 'ide/document.mli')
0 files changed, 0 insertions, 0 deletions