Hi, >>> - 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!
That wouldn't be in background though, right? It'd stop interactive mode in the file I was in. Kind regards, Ralf _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
