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...
ProofGeneral-devel mailing list
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.