On Monday 06 December 2010 14:14:27 David Aspinall wrote: > Pierre and I had investigated a few ideas, > you can still see some code remains in coq.el from some old attempts > that partly worked (auto-compile-vos), but it seemed that Coq users were > never hugely interested in the feature. > It would be more interesting, if the compilation reused the coqtop state obtained while processing the buffer. Currently every file is actually compiled twice. So nobody would reasonably process the whole buffer after having edited it somewhere in the middle just to trigger the automatic compilation. Also, a completely processed buffer doesn't seem to be retracted when starting to process another buffer. This is not what you want in Coq where the environment remains polluted by the definitions made in the other module.
But the mechanism Hendrik proposes sounds very useful, so good luck! -- Paolo Herms PhD Student - CEA-LIST Software Safety Lab. / INRIA ProVal Project Paris, France _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
