Hi, >>> 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, Ralf _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
