Processing multiple commands terminated with a comment doesn't update proof state

[tchajed]

In the following example,

Goal True.
    trivial. (* *)
Qed.

if you process the auto and comment together (you can just goto the end of the comment), then the proof state is not refreshed until you do something like C-c C-p. For example, if Goal True. is part of this goto, then there is no proof state, and if you run just trivial. (* *) then you'll still see a goal of True even though it's been solved.

This only seems to happen if the last sentence in a sequence of commands sent together is a comment. Processing a command in the middle of a sequence works correctly.

[Matafou]

I was aware of this bug but strangely I did not find a corresponding bug report.

Thanks for reporting, we will see if we fix this now or after switching to the new protocol.

[psteckler]

I can verify the bug in the current PG, and also verify that it does not
occur in the XML protocol fork.

-- Paul

On Wed, Aug 17, 2016 at 11:47 AM, Pierre Courtieu [email protected]
wrote:

I was aware of this bug but strangely I did not find a corresponding bug
report.

Thanks for reporting, we will see if we fix this now or after switching to
the new protocol.

—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub
#102 (comment),
or mute the thread
https://github.com/notifications/unsubscribe-auth/ACJAKHARK3fYkggNsu4PqjoGQj0U6iVfks5qgyz0gaJpZM4Jmkxm
.