Custom Query (361 matches)
Results (40 - 42 of 361)
| Ticket | Resolution | Summary | Owner | Reporter |
|---|---|---|---|---|
| #111 | fixed | Centering the goal window on the right part of the goals | ||
| Description |
In coq, when doing large proofs, the goals window tends to not be centered on the right information: it only shows the oldest assumptions, and when the list of assumption is too long, it does not even show the statement of the first goal.
I suggest centering on bar of equal signs that separates the most recent hypotheses from the current goal. I did it by modifying two files: proof-utils.el and pg-goals.el
While I think that the modification on proof-utils.el can be shared with other proof
systems (I only add the possibility that the target point could be given by a string
that will be searched in the buffer), the change done on pg-goals.el is coq-specific
and should not be left there, but I could not find how to make the code customizable in this respect. So this is a suggestion for modification, but this should be reviewed to make it more generic in its approach. |
|||
| #217 | wontfix | Chosen logic: changes should invoke isabelle-load-isar-keywords | ||
| Description |
Chosen logic can now be changed using file local variables as well as menu. To be precise, either way should reload the appropriate keywords file and refresh. |
|||
| #402 | wontfix | Clean up customization groups/settings | ||
| Description |
The customization groups for Proof General need a bit of tidying: for example, the Proof General Internals group and Prover Config group has settings which appear as CHANGED or UNINITIALIZED. These probably don't cause any problems in everyday use but are odd to users who browse Customize options. |
|||
