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. -- Paul 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. > _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
