Re: [PG-devel] -quick

>> 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

Re: [PG-devel] -quick

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

Re: [PG-devel] -quick

Hi, >> Ah, that's a good point. I should try that one time. Thanks for the hints! > > And if you define that procedure (changing to the import all > file, doing C-c C-b there) as an emacs macro, then you can start > the whole recompilation with just one key stroke. Right, but on the other

Re: [PG-devel] -quick

> wiring M-x compile to "make vio2vo J=X" and then wiring that to a > shortcut is going to be simpler. (I didn't even know about M-x compile FWIW, I happily use (global-set-key "\C-c\C-c" 'compile) Stefan ___ ProofGeneral-devel mailing

Re: [PG-devel] -quick

Ralf Jung writes: > Ah, that's a good point. I should try that one time. Thanks for the hints! And if you define that procedure (changing to the import all file, doing C-c C-b there) as an emacs macro, then you can start the whole recompilation with just one key stroke.