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
