2011/1/12 Hendrik Tews <t...@os.inf.tu-dresden.de>
> 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.
I don't understand what you mean by "retracted changing the scripting
buffer". Commands are retracted when the user goes back in the script. If
you go back to point scripted before the invisible command has been sent, it
should retracted as well.
> Is this really a feature? Do I have to add a corresponding
> proof-deactivate-scripting-hook to undo the effects?
ProofGeneral-devel mailing list