On 2016-07-08 19:06, Paul A. Steckler wrote: > So when you edit in a buffer, you send an StmCancel messages, you > get messages for each cancelled state, so you can just mark the > corresponding overlays appropriately. Yes?
Indeed, SerCoq makes things simpler here. With EditAt you send an EditAt instead of Cancel, but it's essentially the same otherwise in terms of messages sent. The one difference is in the response: SerCoq sends me individual Cancelled messages, whereas EditAt send you a single message with two state IDs indicating a range: > Maybe it would be better to lock the individual spans for each > sentence, as I think you've done in elcoq. Yes, I think that would be the simplest. With EditAt you'll get a pair of states to cancel, which stands for a "geographical" range. For examples if states IDs are 1 8 18 6 3 9 and you get (18,9), you should cancel 18,6,3,9. The function overlays-in should help for this.
Description: OpenPGP digital signature
_______________________________________________ ProofGeneral-devel mailing list ProofGeneralemail@example.com http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel