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 <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
> 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@inf.ed.ac.uk
> http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to