Opened 16 years ago
Closed 15 years ago
#211 closed enhancement (fixed)
Coq : deactivation of the 'Holes' functionality
Reported by: | coquser | Owned by: | David Aspinall |
---|---|---|---|
Priority: | minor | Milestone: | PG-Emacs-4.0 |
Component: | 2:pg-emacs | Keywords: | |
Cc: |
Description
The manual mentions a 'Holes' feature in section §9.5. It seems that it activates as soon as the abbrev mode is loaded when opening a coq source file (.v), and appends its predefined abbreviations to the current abbrev table (if it already exists).
It is my understanding that this behavior forces quite a few abbreviations upon the user that fancies using emacs' abbrev-mode, without any way to deactivate this feature, short of editing the source code manually.
I'm using ProofGeneral to edit SSReflect Coq files (a syntaxic - among others - extension for Coq that makes the predefined abbreviations irrelevant), and would like to use the abbrev-mode without any modification of my abbrev-table.
Is there a way to deactivate the Holes feature that I have missed ?
Change History (3)
comment:1 Changed 16 years ago by
Milestone: | PG-Emacs-3.7.1 → PG-Emacs-3.7.2 |
---|---|
Owner: | changed from courtieu to David Aspinall |
Status: | new → assigned |
comment:2 Changed 16 years ago by
Milestone: | PG-Emacs-3.7.2 → PG-Emacs-4.0 |
---|
comment:3 Changed 15 years ago by
Resolution: | → fixed |
---|---|
Status: | assigned → closed |
The patch seems ok to me.
holes completion in abbreviations is now disabled if (customizable) variable coq-holes-minor-mode is set to nil.
I think we should allow the Holes feature to be turned off. To do this smoothly perhaps the holes symbols could be replaced by underscores in the insertion functions defined in coq.el which suppose holes are available.
But meanwhile, it looks as if the code intended not to trash your (local) abbrev table was faulty. I've patched it.