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 <> wrote:
> 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?
> P.
> 2016-06-30 17:40 GMT+02:00 Paul A. Steckler <>:
>> 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
>> PG.
>>   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

Reply via email to