aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2017-02-16 14:14:34 +0100
committerEmilio Jesus Gallego Arias2017-04-12 16:18:08 +0200
commit3a7d9fcafedc4987d0748a8717b2b012a779de39 (patch)
tree59bded0fc995c7a9137f909832592a9c8ee8807f /dev
parentb209cea412a9541fd1c434dde36ea6eb1e256a33 (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 'dev')
0 files changed, 0 insertions, 0 deletions