Print Fully Explicit option gets out of sync after undoing before point where it was changed

[Robin Green]

This has been a bug in PG for several years now, but as far as I can see I haven't reported it before.

If you select or deselect the setting Print Fully Explicit, and then immediately do proof-undo-last-successful-command, the setting will be reverted to its previous state, but PG still thinks it is enabled (or disabled, whichever you set it to be).

I don't know if this also occurs with other settings.

If I recall correctly, you can get back in sync again by toggling the option in emacs, which has no effect on Coq.

[David Aspinall]

Confirmed, thanks for the report.

We need to discuss this point with the Coq developers. It surprises me that the value for a flag for printing output is recorded in the undo state. PG doesn't have generic support for recording the values of such flags (or interrogating them) at different points in the script. That could be added, although it seems barely worth it.

Does the undo behave correctly if the command is added to the script?

[David Aspinall]

What about if we remove the variable and menu command? It doesn't seem helpful to users but would shake out what people and Coq implementation wants as the intended behaviour.

[David Aspinall]

An alternative "fix" would be to have the menu command insert the text into the buffer and assert it, but this may mess up this script.

[courtieu]

I just removed this kind of command from the settings menu. I added a "option" menu that don't try to keep track of the values of variables. I mark this bug s fixed.