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.
>>
> 

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