Custom Query (361 matches)
Results (52 - 54 of 361)
| Ticket | Owner | Reporter | Resolution | Summary |
|---|---|---|---|---|
| #230 | wontfix | Configuration simplification: unify regexp/function settings | ||
| Description |
Goal/save settings use strings (for regexps) and functions. We can unify the setting and let the prover choose either, provided it can work also for imenu/speedbar. |
|||
| #231 | wontfix | Consider replacing maths-menu for token mode with own version | ||
| Description |
Instead of using maths-menu, we may configure the menu automatically from the token tables, so including the exact set of tokens and tokens also for compositions (which are not displayable in menus, however). To do this, the mode specific tokens may be collected into separate planes as in the current maths menu, so we need some nested structure with headings in the main table. |
|||
| #257 | invalid | Byte Compilation fails because of comments in the completion file | ||
| Description |
I have a problem in a byte compilation of 'Proof General 3.7.1' with emacs-22.1.50 on Mac OS X 10.5.5. 'make compile' failed with an error: In toplevel form: generic/pg-user.el:24:13:Error: Invalid read syntax: "#" make[2]: * [generic/pg-user.elc] Error 1 make[1]: * [.byte-compile] Error 2 make: * [compile] Error 2 when my completion file (~/.completion) has commented-out lines starting with "#". The compilation was successfully completed after removing the comments in the file. |
|||
