David Aspinall <david.aspin...@ed.ac.uk> 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, possibly, the library itself and some
of its dependencies must be recompiled.
check compiled files are up to date. I'm not sure whether the file
save/load hooks would be more appropriate than a hook run when command
is queued, or whether connecting to standard Emacs make mechanisms
would be sensible.
Using some file save hook is an interesting idea... but it doesn't
run when you check out from a repository ...
For your way, maybe the standard
proof-shell-insert-hook would work? This runs when a command is
actually sent to the process, versus when it is queued.
proof-shell-insert-hook is run when a command is taken from a the
queue and send to the proof assistent, right?
IMO asking for recompilation when the command is sent to coq is
too late. You might script a big buffer and while this runs for
several minutes you start to do anything else. Then in the middle
of this anything you would get interrupted with the question for
recompilation. I would prefer to finish recompilation before eg.
proof-goto-point or proof-assert-next-command-interactive finish.
Which hook is run when a command is queued?
http://proofgeneral.inf.ed.ac.uk/trac/ticket/363
I would prefer to stay on the mailing list, if possible.
Bye,
Hendrik
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
