> 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 SetLoadPath. > 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 scripts? - D. _______________________________________________ ProofGeneral-devel mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
