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?

ProofGeneral-devel mailing list

Reply via email to