Re: [PG-devel] setting completion-ignored-extensions
>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. > Additionally completion-ignored-extensions are hidden by default > in dired buffers. Not by default, no. They are highlighted with a different face (the face is `dired-ignored'), but you need to activate dired-omit for them to be actually hidden. Stefan ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] setting completion-ignored-extensions
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 http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] setting completion-ignored-extensions
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 dired buffers. Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] setting completion-ignored-extensions
>> 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 will do the trick. > Much neater idea... although at the moment our autoloads are only generated > for the generic code and one might hope that e.g. using Isabelle doesn't > automatically make .vo files unreadable -- in case Isabelle would use that > extension for something else (it probably doesn't, but). completion-ignored-extensions only tells completion to prefer files with other extensions. So you can still read those files just fine if you don't rely too heavily on completion. They even still appear in *Completions*. So it's usually pretty harmless. 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, regardless of whether you have a .vo file or not and if you've added .vo to completion-ignored-extensions. The only case where it would make a difference is when you have a .v8 file (or some such extension) where the presence of a .vo might cause completion of "foo" to stop at "foo.v" rather than go all the way to "foo.v8". Stefan ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] setting completion-ignored-extensions
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 will do the trick. Much neater idea... although at the moment our autoloads are only generated for the generic code and one might hope that e.g. using Isabelle doesn't automatically make .vo files unreadable -- in case Isabelle would use that extension for something else (it probably doesn't, but). - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] setting completion-ignored-extensions
> 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 I suggested, to extend > proof-assistant-table with one row for ignored extensions. This > is not particularly nice, because Coq will be the only one that > uses this row. 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 will do the trick. Stefan ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] setting completion-ignored-extensions
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 I suggested, to extend proof-assistant-table with one row for ignored extensions. This is not particularly nice, because Coq will be the only one that uses this row. I suppose you are right, it should be set early and it makes sense to put in proof-assistant-table because that configures the main file name extensions. Do you want to try that? Watch out for the AUTOMODE-REGEXP optional last column (not currently used but was in the past). - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] setting completion-ignored-extensions
David Aspinall 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. 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 I suggested, to extend
proof-assistant-table with one row for ignored extensions. This
is not particularly nice, because Coq will be the only one that
uses this row.
If you don't like changing proof-assistant-table, my suggestion
is the following: In proof-site.el I add a new defcustom
proof-general-completion-ignored-extensions with default value
'(".vo" ".glob"). Additionally, somewhere in proof-site.el the
contents of proof-general-completion-ignored-extensions is added
to completion-ignored-extensions.
Bye,
Hendrik
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] setting completion-ignored-extensions
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.
Cheers,
- David
On 29/03/11 12:08, Pierre Courtieu wrote:
OK then.
Cheers,
P.C.
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"
".pyo")
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.
Bye,
Hendrik
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
Re: [PG-devel] setting completion-ignored-extensions
OK then.
Cheers,
P.C.
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"
> ".pyo")
>
> 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.
>
> Bye,
>
> Hendrik
> ___
> ProofGeneral-devel mailing list
> ProofGeneral-devel@inf.ed.ac.uk
> http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
>
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] setting completion-ignored-extensions
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"
".pyo")
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.
Bye,
Hendrik
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] setting completion-ignored-extensions
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 : > 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 > ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
