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

Reply via email to