Followup for discussion started in #28.
Relevant quotes:
One remark for possible future work is that since you are using the XML protocol, it should be possible (in theory, IIRC) to do partial rollbacks (e.g. within a proof that is ended by a Qed) without necessarily rolling back what follows. @gares could say more about this. But this poses problems with how to handle Qed so I'm not really sure it's worth to actually look into.
About fixing broken proofs: the result of the edit_at message signals if the edition is in a script fragment that can be edited without invalidating the rest (typically the text between Proof and Qed). I tried to look at your code but I could not find where you interpret the answer to the command edit_at.
See the doc of the ML API: https://github.com/coq/coq/blob/master/stm/stm.mli#L128
https://m.youtube.com/watch?v=OAoVHoeXSgk
Followup for discussion started in #28.
Relevant quotes: