Ralf Jung <j...@mpi-sws.org> writes:

>> - you start scripting in file A (for instance to fix a proof)
>>   while compile-everything is still in progress? Have 2
>>   compilations in parallel or abort compile-everything?
>
> Aborting when the active file is changed sounds fine. I guess that's
> what vio2vo also does in background?

OK, how about creating a emacs macro that does C-c C-b in the
file that imports everything? You can easily bind this to F9 or
or any other key - then you get everything with just one
keystroke!

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

Reply via email to