This is not entirely true. The backtrack mechanism of coq/pg is more robust
than that, thanks to state numbers of coq you can undo most invisible
commands by going back to a point in the file that was scripted before the
invisble command. However LoadPath is probably not part of the undo model
and Coq does not retract them when going back to a previous state.
Hendrik I don't understand why you need to add a load path by yourself. The
user should have put -I options to coqtop from the beginning, no? Or they
should have put LoadPath in there files. Or is it that you want to parse the
required file itself??
I would suggest you do not try to alter coqtop options, as users already
know how to do that. I recommend using file variables in each coq file and
restart coq when changing file so that the correct command line is used. As
you said: in coq one must retract a file before starting a new one, so
restarting Coq is not a problem: it takes no time.
So I plan to use your feature by using another file variable:
(*
*** Local Variables: ***
*** coq-prog-name: "coqtop" ***
*** coq-prog-args: ("-I" "." "-I" "../../ALEA/src") ***
*** coq-load-path: ("../../ALEA/src") ***
*** End: ***
*)
The only improve I see is to use coq-load-path to set coq-prog-args when
opening a new file.
P.
2011/1/13 David Aspinall <david.aspin...@ed.ac.uk>
> > 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
> > deactivated.
>
> proof-shell-invisible-command is designed for sending diagnostic and
> control commands which are not scripting commands and not part of the undo
> model of the prover. You only get undo behaviour for commands which appear
> in the buffer text.
>
> So, yes, you may need to adjust the load path manually with the scriting
> activate/deactivate hooks.
>
> - D.
>
> _______________________________________________
> ProofGeneral-devel mailing list
> ProofGeneral-devel@inf.ed.ac.uk
> http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
>
> --
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
>
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
