> 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 

 - D.

ProofGeneral-devel mailing list

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Reply via email to