defpacustom and undo

[coquser]

Hi,

defpacustom settings are not preserved over undo, at least not for Coq. Consider, for instance, switching "Print fully explicit" on in the middle of some file, then after undo, you get again normal printing behavior. (For Coq, this is of course not really surprising.) I don't know, if we really want to implement settings that are preserved over undo. However, it would be nice, if the defpacustom variable is reset to normal state (and thereby also its menu entry), if its effect is lost because of an undo.

Hendrik

[David Aspinall]

Already noted in #419. For what it's worth, my opinion is that commands which change the prover state like scripting commands (i.e. are undoable) should be recorded in the script. So a "fix" here would be to remove the defpacustom setting.