Opened 17 years ago
Closed 17 years ago
#111 closed defect (fixed)
Centering the goal window on the right part of the goals
Reported by: | Yves Bertot | Owned by: | David Aspinall |
---|---|---|---|
Priority: | major | Milestone: | PG-Emacs-3.7 |
Component: | 2:pg-emacs | Keywords: | |
Cc: |
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.
Attachments (2)
Change History (3)
Changed 17 years ago by
Attachment: | pg-goals.el added |
---|
Changed 17 years ago by
Attachment: | proof-utils.el added |
---|
proof-utils.el with a modification to the function proof-display-and-keep-buffer, to make it able to receive a string as optional argument
comment:1 Changed 17 years ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
Replying to bertot:
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.
For the moment I commited a patch I have been using at home for a long time. It is in coq specific directory. I agree that something more general would be good.
The patch is not exactly as yours: it scrolls to the bottom of the current goal (don't show the others if any). So if goal is bigger that the window then only its end is visible. I am not sure this is the best. Let me know.
by the way, to make your patch "coq specific", you probably need to us the hook: proof-shell-handle-delayed-output-hook.
I make this bug "fixed" but don't hesitate to re-submit something if this is not satisfactory.
Cheers, P.C.
pg-goals.el with my modification, which should be cleaned up by a more competent developer.