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
