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 the only supported prover that compiles files at the moment.


 - David

On 29/03/11 12:08, Pierre Courtieu wrote:
OK then.


2011/3/29 Hendrik Tews<>:
Pierre Courtieu<>  writes:

   I agree with the idea, but should we really modify
   completion-ignored-extensions by ourselves?

That's the usual practice. Here emacs -q -no-site-file gives

    completion-ignored-extensions is a variable defined in `C source code'.
    Its value is
    (".o" "~" ".bin" ".lbin" ".so" ".a" ".ln" ".blg" ".bbl"
    ".elc" ".lof" ".glo" ".idx" ".lot" ".svn/" ".hg/" ".git/"
    ".bzr/" "CVS/" "_darcs/" "_MTN/" ".fmt" ".tfm" ".class"
    ".fas" ".lib" ".mem" ".x86f" ".sparcf" ".fasl" ".ufsl" ".fsl"
    ".dxl" ".pfsl" ".dfsl" ".p64fsl" ".d64fsl" ".dx64fsl" ".lo"
    ".la" ".gmo" ".mo" ".toc" ".aux" ".cp" ".fn" ".ky" ".pg"
    ".tp" ".vr" ".cps" ".fns" ".kys" ".pgs" ".tps" ".vrs" ".pyc"

   Is it not considered a
   user preference? Some people dislike hiding files at all.

Those people must then switch off the effects of
completion-ignored-extensions on a different level, so they won't
even notice if we add another two elements.


ProofGeneral-devel mailing list

ProofGeneral-devel mailing list

ProofGeneral-devel mailing list

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Reply via email to