On 2016-07-09 21:18, Paul A. Steckler wrote: > Looking at CJ's notes, I see that you only get a pair of state id's > when there's a new focus. Otherwise, you just get a single state_id, > which is the new tip. > > That will make it easy to determine when to use a pair of locked > spans, or just one of them.
Yup, absolutely. > > On Sat, Jul 9, 2016 at 2:30 AM, Clément Pit--Claudel > <clement....@gmail.com> wrote: >> 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 ProofGeneralfirstname.lastname@example.org http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel