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?
ProofGeneral-devel mailing list