2011/1/13 David Aspinall <[email protected]> > > 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 [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
