>>> 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!
>> That wouldn't be in background though, right?  It'd stop interactive
>> mode in the file I was in.
> If I understood correctly, you wanted to compile the whole
> project after finishing some change in one of the files. This is
> what you get here: You process the require commands in the
> import-all file, thereby compiling everything in your project that
> is outdated. Then you wait for the first error in
> *coq-compile-respone*, when you see one, you can go there to
> examine the situation. Meanwhile the background compilation will
> go on as far as possible, possibly producing more errors in
> *coq-compile-respone*. 

Ah, that's a good point.  I should try that one time.  Thanks for the hints!

Kind regards,
ProofGeneral-devel mailing list

Reply via email to