I agree with Hendrik, activate-scripting is not the right trigger
because dependencies may change *after* scripting is activated. Each
time the user adds "Require Import foo." and scripts it, proofgeneral
should try to compile foo.v if it is not up-to-date. The cvs update is
also a good point.
2010/12/10 Hendrik Tews <t...@os.inf.tu-dresden.de>:
> David Aspinall <david.aspin...@ed.ac.uk> writes:
> Did you consider the scripting time option, file activated for
> scripting? This is the place that saves of potential-ancestor files
> What precisely do you mean? Do you mean ProofGeneral's concept of
> the active scripting buffer and proof-activate-scripting-hook?
> I don't want a solution based on proof-activate-scripting-hook,
> because I want to update files outside of emacs (eg by cvs
> update) while I am scripting in some buffer.
> ProofGeneral-devel mailing list
ProofGeneral-devel mailing list