Pierre Courtieu <pierre.court...@cnam.fr> writes:


   2011/1/12 Hendrik Tews <t...@os.inf.tu-dresden.de>

   > 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.

   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

Sorry, in more detail: In your example from yesterday, one
indirectly required file was in a different directory, say
"other-dir". In order to get this running other-dir must be put
into coq-load-path. Further, the contents of coq-load-path must
be passed to invocations of coqdep and coqc via -I options. All
this does work now: the dependencies are computed and the files
are recompiled correctly (see cvs head).

And now to the problem: In order to process the Require command
in the scripting buffer, coq-load-path must also be put into
coqtop, which is running behind. To achieve this I decided to add
a function to proof-activate-scripting-hook. This function sends
"Add LoadPath" for each element of coq-load-path via

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


ProofGeneral-devel mailing list

Reply via email to