2011/1/13 Pierre Courtieu <pierre.court...@cnam.fr>
> 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??
>
To be more precise, nowadays in order to script a Require the user already
must have put the right directory in the load path. So why do you need to
add more?
> 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
