Implement partial rollbacks

[EugeneLoy]

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