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 proof. I think Emilio was suggesting that you also
get something indicating the end of that proof, and it's up to PG to
find the contained spans. I might handle that by having two locked
spans, instead of the single one PG now uses. Maybe it would be better
to lock the individual spans for each sentence, as I think you've done
On Fri, Jul 8, 2016 at 12:23 PM, Clément Pit--Claudel
> I think I got that working fine in elcoq. Did you have a look?
> 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, the sentence spans are glued
>> I've gotten rid of the gluing step, and now undo will work with the
>> steps of a completed proof.
>> But I think the async mode will require something more complex,
>> because there can be multiple parts of the script that have been
>> processed, interleaved with unprocessed parts.
>> It looks like the Stm machinery gives the dependencies between parts
>> of the script, and it may be the key to structuring spans. Do we know
>> if that's available through the XML interface?
>> -- Paul
>> On Fri, Jul 1, 2016 at 4:43 AM, Pierre Courtieu <pierre.court...@cnam.fr>
>>> I cc Enrico for this one.
>>> In pg/coq there should be one span at a time (but emacs uses overlays
>>> for other purposes). When a proof is finished (Qed or Save) the spans
>>> of the proof are glued together in a single span on the whole lemma.
>>> Coq's backtracking mechanism used to be unable to backtrack inside a
>>> proof and I never implemented a "replay" feature to workaround it.
>>> There is probably a way to avoid the glueing.
>>> But with the Stm machinery (do you use it Paul?) it should be much
>>> simpler to deal with spans. Enrico can you say a word on this?
>>> 2016-06-30 17:40 GMT+02:00 Paul A. Steckler <st...@stecksoft.com>:
>>>> Hi all,
>>>> I'm making decent progress on getting PG to work with the Coq
>>>> XML(ish) protocol.
>>>> The main stumbling block I'm having is making sure the spans have
>>>> the correct structure. Those are implemented by Emacs overlays.
>>>> Can someone explain what the structure of the spans should be, and
>>>> what metadata they should contain? Are there invariants that should
>>>> hold as a user steps through a proof?
>>>> I'm told that CoqIDE has a similar notion, but there's just one span
>>>> per sentence in a script. I'm noticing multiple, overlapping spans in
>>>> Currently, PG has machinery to know where a proof begins. If you
>>>> undo just past a finished proof, the entire proof is retracted. I'm
>>>> told that since 8.5, you can backtrack to the middle of a proof, so
>>>> that machinery is unneeded.
>>>> -- Paul
>>>> ProofGeneral-devel mailing list
>> ProofGeneral-devel mailing list
> ProofGeneral-devel mailing list
ProofGeneral-devel mailing list