> I expected, that when changing the buffer and retracting the old > scripting buffer, all those Add LoadPath commands are retracted as > well. However, this is not the case! Commands sent via > proof-shell-invisible-command from inside > proof-activate-scripting-hook are not retracted when scripting is > deactivated.
proof-shell-invisible-command is designed for sending diagnostic and control commands which are not scripting commands and not part of the undo model of the prover. You only get undo behaviour for commands which appear in the buffer text. So, yes, you may need to adjust the load path manually with the scriting activate/deactivate hooks. - D. _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk 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.
