Custom Query (361 matches)
Results (52 - 54 of 361)
| Ticket | Resolution | Summary | Owner | Reporter |
|---|---|---|---|---|
| #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. |
|||
| #258 | fixed | Copying from response buffer also copies colour control chars | ||
| Description |
In the latest CVS (updated Oct 28th, but problem existed previously): If I copy something colourful from the response buffer, like say a green "xs", when I paste it into the proof (text) buffer, I'll get something like AFxsAA. Copying subgoals out of the response buffer and proving them as separate (generalised) lemmas is a common use-case for me. I'm using Isabelle/HOL. |
|||
