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 function in the hook that looks for
require commands and takes appropriate actions. The hook variable
itself should be buffer local, to avoid that the
coq-require-filter function is called in an Isabelle session.

Any comments?

Bye,

Hendrik
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to