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.

Attachment: signature.asc
Description: OpenPGP digital signature

_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to