2011/1/13 David Aspinall <david.aspin...@ed.ac.uk>

>
>  For getting correct multiple file scripting for coq I would first
>> try to restart coqtop on every new scripting buffer. What would
>> be the best way to achieve this? Put proof-shell-exit into
>> proof-deactivate-scripting-hook?
>>
>
> I suppose but this does seem pretty crude, there is some cost to setting
> up/tearing down process and associated buffers, etc.
>
> Doesn't something like Reset Intial work (restart button's command)?
>
>
No, for the same reason backtrack does not work. Add LoadPath is considered
transient by coq.


>     >  will be sufficient. The -I arguments can be derived from
>>    >  coq-load-path and coqtop is default.
>>    >
>>    >
>>    That would be nice. For this we can ask David to allow prog-args to be
>> a
>>    function instead of a list. In proof-shell near line 239. This way we
>> can
>>    define coq-prog-args as the function that build the -I list from
>>    coq-load-path.
>>
>> I would leave prog-args as it is now. I view coq-prog-args as the
>> place for options different form -I and -R like -is or
>> -impredicative-set.
>>
>
> I suppose Pierre means that you need a way to influence the command line
> calculation as you wanted, perhaps with yet another control function/hook or
> variable for prog-args (already several added for Coq..).
>

That's exactly what I mean, but i thing Hendrik wants to use Add LoadPath
instead of modifying the command line. This may be a good idea, provided we
are sure that doing Add LoadPath foo. is exactly the same as donig -I foo.

P.
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to