Hi,

AFAICT there is no support for completion-ignored-extensions in
Proof General. For coq, setting completion-ignored-extensions
would be nice, because the coq compiler clutters the directory
with .vo and .glob files.

My suggestion would be to extend proof-assistant-table with one
row for a list of to-be-ignored file-extension. Then the
initialization code in proof-site.el could extend
completion-ignored-extensions appropriately.

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