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 in elcoq. -- Paul On Fri, Jul 8, 2016 at 12:23 PM, Clément Pit--Claudel <clement....@gmail.com> wrote: > I think I got that working fine in elcoq. Did you have a look? > > Clément. > > 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 >> together. >> >> 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> >> 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 <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 >> > > > _______________________________________________ > 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
