> Undoing those Add LoadPath commands with Remove LoadPath commands
> would be rather difficult. If one adds a directory which is
> already in the LoadPath, coq reorders the LoadPath, a subsequent
> remove will not yield the starting state.
In that case I'm not sure how you can achieve what you need, unless there is
> proof-shell-invisible-command is designed for sending
> diagnostic and control commands which are not scripting
> OK, is there an alternative that I could use from inside
> proof-activate-scripting-hook in order to get undo behaviour?
No, invisible command is the only thing open to you.
In any case, Proof General is nowadays (intentionally) quite stupid about undo
commands and just points Coq at particular states in its internal history based
on counting script commands sent.
Maybe Pierre can advise (or has already advised) on whether the load path is
part of the state that Coq manages internally in its history. If it isn't then
you're not going to get something automatic.
To manage things manually, you could add special properties to the spans in the
buffer to record the loadpath before an adjustment is made, then alter Coq's
undo calculation to issue commands to restore the value when those regions get
retracted. Sounds doable, but tedious. How often is AddLoadPath used in
ProofGeneral-devel mailing list
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.