I think it is available. But I a mnot sure we should reflect async
proof yet. Let us have PG work as before, then we make the async proof
queue working.
P.
2016-07-07 22:07 GMT+02:00 Paul A. Steckler :
> It looks like there are is a span representing the locked region of
> the entire script, and
On Fri, Jul 8, 2016 at 5:35 AM, Enrico Tassi wrote:
> On Fri, Jul 08, 2016 at 10:10:49AM +0200, Pierre Courtieu wrote:
>> I think it is available. But I a mnot sure we should reflect async
>> proof yet. Let us have PG work as before, then we make the async proof
>> queue working.
>
> As far as I k
I think I got that working fine in elcoq. Did you have a look?
Clément.
On 2016-07-07 16:07, Paul A. Steckler wrote:
> It looks like there are is a span representing the locked region of
> the entire script, and then one span apiece for individual sentences.
> When the end of a proof is reached,
Yes, just looked at it again.
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?
With Edit_at, you get back a value tag indicating the current state id
within a re-opened proo
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
