Custom Query (361 matches)
Results (43 - 45 of 361)
| Ticket | Owner | Reporter | Resolution | Summary |
|---|---|---|---|---|
| #199 | fixed | Allow use of Isabelle.command to wrap commands singly | ||
| Description |
Isabelle.command allows additional "properties" to be attached to individual commands when they are processed by Isar. Example properties are file name and line number (Isabelle Position type), which are not maintained by the top-level loop, but would be useful to get error messages to include this information when processing interactively. |
|||
| #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 ? |
|||
| #216 | wontfix | Toolbar size on Carbon Emacs | ||
| Description |
A user reported toolbar size problems with latest Carbon Emacs. |
|||
