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)?

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

I suggest refactoring the setting of prog-command-line in proof-shell-start into a new function which does this, so (proof-shell-prog-command-line) returns the command line you want. That would clear up the beginning of proof-shell-start a bit.

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

Reply via email to