Re: [PG-devel] Span (overlay) structure in PG

[Clément Pit--Claudel]

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



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

Re: [PG-devel] Span (overlay) structure in PG

[Paul A. Steckler]

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

Re: [PG-devel] Span (overlay) structure in PG

[Clément Pit--Claudel]

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.



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