Vadim Zaliva (Nov 22 2023 at 23:28): Vadim Zaliva (Nov 22 2023 at 23:28):If there is a way to customize status line in goals buffer? I really want it to show number of goals. I am using PG+CompanyCoq.
Pierre Courtieu (Nov 24 2023 at 08:44):Hi. You should already see the number of goals in the modeline (of the buffer being scripted), but it is a bit raw: it show the number of goals currently under focus. It should be relatively simple to make this better when Set Printing Unfocusedis set, but it is not implemented yet.
Vadim Zaliva (Nov 24 2023 at 08:54):Ah, I can see it now (after I disabled doom-modeline-mode). Thanks! I was looking for it in the "goals" buffer. Any way to make it work with it or better yet to add the number of goals display via simple hook modifying mode line variable for goals buffer?
Pierre Courtieu (Jan 21 2024 at 15:50):Sorry to come to this months after your question. This seems possible. Not sure we have much time for it. Of course if someone proposes a patch we would be glad to review and merge it.
Axel Daboust (Apr 02 2024 at 14:17):Hi. I recently proposed a fix with a PR #755 that enables information visible in the goals buffer modeline (it also clears the goals buffer when skipping a proof) . As my first contribution to this project, I'd be glad to receive some pieces of advice on enhancement of the feature, or even some other issues I could work on. Thanks in advance !
Pierre Courtieu (Apr 03 2024 at 07:46):Hi. Thanks for your PR. I just made a review.
Pierre Courtieu (Apr 03 2024 at 07:47):What kind of other fix would you like to fix (we welcome that!).
Axel Daboust (Apr 03 2024 at 12:57):Many thanks for your review ! I think I will browse issues on PG, but I wondered if you had fixes in mind that were "urgent" and that could save you some time of digging.
Vadim Zaliva (Apr 03 2024 at 15:54):@Axel Daboust thanks for working on this! By the way, here is my workaround (adding the following hook in coq). (add-to-list 'global-mode-string '(" " (:eval (assq 'proof-active-buffer-fake-minor-mode minor-mode-alist))) " ") I am not sure how you implemented it but you may find this helpful.
Axel Daboust (Apr 03 2024 at 15:59):@Vadim Zaliva You're welcome ! Thanks for your tip, it may help making the solution cleaner.
Last updated: Oct 13 2024 at 01:02 UTC