>>> - 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,
ProofGeneral-devel mailing list

Reply via email to