CoqIDE processed state isn't updated upon pasting to the buffer

[Alizter]

Write some axioms/definition in the buffer, for example

Axiom A : Type.

Step down so it is highlighted. Next select everything and paste the following (replacing the content of the buffer):

Check A.

Step down, and see that this succeeds! Even though Axiom A is no longer in the buffer at all. The proof state seems to think it is.

Originally posted by @Alizter in #15861 (comment)

[eponier]

I also faced this issue. It probably means I did not test enough Pierre-Marie's patch.

It can also be triggered with undo/redo and even just manual deletion of processed text. Sometimes you can write again and sometimes not. In the second case, if you move the processed cursor backwards, you can see it cancels what you've just removed, meaning that it indeed still believes it is in the document. When you're in sync again with the document, everything works again.