Skip to content

add customizable variables to configure which part of a goal the goal buffer will focus on #654

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

add customizable variables to configure which part of a goal the goal buffer will focus on #654

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
51dc549
add customizable variables to configure which part of a goal the goal
May 23, 2022
f35d937
Update coq.el
cipher1024 May 27, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 21 additions & 5 deletions coq/coq.el
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -115,6 +115,18 @@ Namely, goals that do not fit in the goals window."
:type 'boolean
:group 'coq)

(defcustom coq-goal-conclusion-marker "========"
"Marks the part of interest in each goal to focus the goal buffer on"
:type 'regexp
:group 'coq
)

(defcustom coq-center-goal-after-focus 'top
"Where to display the goal marker after rendering a proof goal"
:type '(radio
(const :tag "move conclusion marker to the top of the window" top)
(const :tag "move conclusion marker to the middle of the window" middle)
(const :tag "move conclusion marker to the bottom of the window" bottom)))

Comment on lines +126 to 130
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For better user configuration should we merge this preference with coq-prefer-top-of-conclusion?
Currently if this one is nil then we show the end of the conclusion (of the first goal). Something like:

    (const :tag "focus on the end of the conclusion even if it hides the conclusion marker" tail)

coq-prefer-top-of-conclusioncould be left for compatibilty.
@cipher1024 what do you think?

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I like it! Let's do it

(defconst coq-shell-init-cmd
(append
Expand Down Expand Up @@ -3163,7 +3175,10 @@ buffer."
(goto-char (match-beginning 0))
(buffer-substring p (point)))))))


(defun coq-recenter-goal (loc)
(cond ((eq loc 'top) (recenter 0))
((eq loc 'middle) (recenter nil))
((eq loc 'bottom) (recenter -1))))
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

let us have something like a 'overthetop option?


(defun coq-show-first-goal ()
"Scroll the goal buffer so that the first goal is visible.
Expand Down Expand Up @@ -3192,10 +3207,11 @@ number of hypothesis displayed, without hiding the goal"
;; if the top of concl is hidden we may want to show it instead
;; of bottom of concl
(when (and coq-prefer-top-of-conclusion
;; return nil if === is not visible
(not (save-excursion (re-search-backward "========" (window-start) t))))
(re-search-backward "========" nil t)
(recenter 0))
;; return nil if conclusion marker is not visible
(not (save-excursion (re-search-backward coq-goal-conclusion-marker
(window-start) t))))
(re-search-backward coq-goal-conclusion-marker nil t)
(coq-recenter-goal coq-center-goal-after-focus))
(beginning-of-line))))))))

(defvar coq-modeline-string2 ")")
Expand Down