David Aspinall <david.aspin...@ed.ac.uk> writes: So, yes, you may need to adjust the load path manually with the scriting activate/deactivate hooks.
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. 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? Hendrik _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
