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

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?


ProofGeneral-devel mailing list

Reply via email to