After looking a bit at the code, I believe it is best to install
a new hook, say proof-enqueue-item-hook, that is called in
proof-add-to-queue just before the queueitems are appended to the
proof-action-list. The hook would be called for every item in
queueitems.
coq-mode can then install a func
Hi Hendrik
Thanks for looking at this! 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.
There is some code to take
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 wo
Paolo Herms writes:
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.
I don't understand. Could you elaborate? Why is every file
compiled t
David Aspinall writes:
but it seemed that Coq
users were never hugely interested in the feature.
I just started with coq, but without this feature I will only do
single-file projects.
There is some code to take action after a require has been processed,
This is too late, because, pos
On Monday 06 December 2010 15:38:07 Hendrik Tews wrote:
> I don't understand. Could you elaborate? Why is every file
> compiled twice?
Processing a coq file within emacs means feeding the file to coqtop step by
step. Compiling the file with coqc does pretty much the same thing with the
differenc
Paolo Herms writes:
Processing a coq file within emacs means feeding the file to
coqtop step by step. Compiling the file with coqc does pretty
much the same thing [...]
Thanks for the clarification. I would say the
processing-twice-problem is somewhat orthogonal to detecting
out-of-date
