Re: [PG-devel] setting completion-ignored-extensions

2011-05-11 Thread David Aspinall
To come back on this: I agree that it would be sensible to set completion-ignored-extensions for Coq, given that one does not usually want to open .vo, .glob files in the editor. Hendrik, do you want to add this for Coq? I don't think it needs to be added to generic mechanisms since Coq is

Re: [PG-devel] setting completion-ignored-extensions

2011-05-11 Thread Hendrik Tews
David Aspinall david.aspin...@ed.ac.uk writes: Hendrik, do you want to add this for Coq? Yes, as soon as we agree on how to it best. I don't think it needs to be added to generic mechanisms since Coq is the only supported prover that compiles files at the moment. You are right.

Re: [PG-devel] setting completion-ignored-extensions

2011-05-11 Thread David Aspinall
You are right. However, completion-ignored-extensions should be set up _before_ visiting the first Coq file. That is, it must be initialized when Emacs loads proof-site.el. As far as I can see the only prover specific stuff, which proof-site.el does, comes from proof-assistant-table. Therefore

Re: [PG-devel] setting completion-ignored-extensions

2011-05-11 Thread David Aspinall
As Emacs maintainer I recommend package maintainers to setup their foo-site.el such that it is (mostly if not completely) auto-generated by something like update-directory-autoloads. In such a situation a simple ;;;###autoload (add-to-list 'completion-ignored-extensions .vo) in

Re: [PG-devel] setting completion-ignored-extensions

2011-05-11 Thread Stefan Monnier
As Emacs maintainer I recommend package maintainers to setup their foo-site.el such that it is (mostly if not completely) auto-generated by something like update-directory-autoloads. In such a situation a simple ;;;###autoload (add-to-list 'completion-ignored-extensions .vo) in coq.el