On 10/12/10 14:43, Pierre Courtieu wrote:
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.
This is actually pretty similar to what happens in Isabelle, it is just that Isabelle reports the dependencies to Proof General after it has processed the equivalent of Require (and of course, it reads the file in on the heap at that point rather than compiling).
So, if you don't want to parse the file first you can still use a new hook (or the kludgy wrapper idea, or a modified coqtop top level...) to issue the compile commands exactly when you process Requires, but the rest of the active scripting mechanism could join up well. (Note: when you undo a Require you should unlock the corresponding buffer too.)
It would be great to get this working, but I am remembering why it wasn't so easy...
- D. _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
