Custom Query (361 matches)
Results (88 - 90 of 361)
| Ticket | Resolution | Summary | Owner | Reporter |
|---|---|---|---|---|
| #210 | fixed | input of symbols in Carbon Emacs | ||
| Description |
symbol \<mapsto>. But not in Carbon Emacs. This is quite annoying, because some frequently used symbols have rather long names. Typing them explicitly is a major nuisance. |
|||
| #211 | fixed | Coq : deactivation of the 'Holes' functionality | ||
| 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 ? |
|||
| #213 | fixed | Carbon Emacs: strange unicode abbreviations | ||
| Description |
Carbon Emacs 22.2.1, working with "Unicode Tokens";
typing something like It seems that the unicode abbreviation code does not take the surrounding syntactical context into account. In some situations abbreviations seem to work -- I have no idea yet how to reproduce either behaviour reliably. |
|||
