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