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