Hi, I just noticed the following effect: When I send commands with proof-shell-invisible-command from a member of proof-activate-scripting-hook, then these commands are not automatically retracted changing the scripting buffer.
Is this really a feature? Do I have to add a corresponding proof-deactivate-scripting-hook to undo the effects? Bye, Hendrik _______________________________________________ ProofGeneral-devel mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
