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

2011-05-12 Thread Hendrik Tews
Stefan Monnier writes: But admittedly, it also means that it's mostly useless as well: if your Coq file is called .v the completion will stop at .v in any case, No, it won't, because Coq does also generate .glob files. Additionally completion-ignored-extensions are hidden by default in

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

2011-05-12 Thread Hendrik Tews
Do you want to try that? Watch out for the AUTOMODE-REGEXP optional last column (not currently used but was in the past). Just committed. Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk

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

2011-05-12 Thread Stefan Monnier
But admittedly, it also means that it's mostly useless as well: if your Coq file is called .v the completion will stop at .v in any case, No, it won't, because Coq does also generate .glob files. Indeed adding the .glob extension would be useful, contrary to the .vo I was talking about.

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

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

2011-03-24 Thread Pierre Courtieu
I agree with the idea, but should we really modify completion-ignored-extensions by ourselves? Is it not considered a user preference? Some people dislike hiding files at all. P. 2011/3/21 Hendrik Tews t...@os.inf.tu-dresden.de: Hi, AFAICT there is no support for completion-ignored-extensions