> 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 

So, yes, you may need to adjust the load path manually with the scriting 
activate/deactivate hooks.

 - D.

ProofGeneral-devel mailing list

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

Reply via email to