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
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to