display number of goals in Coq mode

[vzaliva]

display number of goals in Coq mode

[vzaliva]

I dug a little further and the relevant information is shown in proof-active-buffer-fake-minor-mode in mode line. How can I make it displayed by default?

[seagle0128]

According to the snippet below, the info is added to minor mode. So just enbale proof-active-buffer-fake-minor-mode and (setq doom-modeline-minor-modes t).

https://github.com/ProofGeneral/PG/blob/0dd686ec46790e918896670b559b11d38a4bb115/coq/coq.el#L3219-L3227

[vzaliva]

Yes, (setq doom-modeline-minor-modes t) does the trick, but my modeline becomes super cluttered with 9(!) other minor modes shown and does not fit the frame. Is it possible to show just proof-active-buffer-fake-minor-mode in my mode line, not others?

[seagle0128]

If you don't like the default behavior, you can display it in global-mode-string following by the FAQ 5.

e.g.

(add-to-list 'global-mode-string `(" " ,(coq-build-subgoals-string nbgoals nbunfocused)) " ")

PS: I didn't test it. It might be need some tweaks.

[vzaliva]

Thanks. I tried a similar approach, which kind of worked:

(add-to-list 'global-mode-string  `(" " ,(assoc 'proof-active-buffer-fake-minor-mode minor-mode-alist)) " ")

It shows me the number of goals in the mode line, but it is not updated when the number of goals changes. The Proof General code calls force-mode-line-update when the number of goals changes but apparently, it does not affect doom-modeline.

[seagle0128]

(add-to-list 'global-mode-string  `(" " ,(assoc 'proof-active-buffer-fake-minor-mode minor-mode-alist)) " ")

This doesn't work while the number changes, since it won't be evaluated. You should use function or eval to force to update.

[vzaliva]

I don't know how to do that. This is a static list. How can I add a function which evaluates later into it?

I want to point out that the Proof General code forces updates of proof-active-buffer-fake-minor-mode string when the number of goals changes. It just did not get propagated to doom-modeline.

[seagle0128]

Try this

(add-to-list 'global-mode-string '(" " (:eval (coq-build-subgoals-string nbgoals nbunfocused))) " ")

[vzaliva]

There are no nbgoals and nbunfocused variables. They are local variables in coq-update-minor-mode-alist function, not exposed outside.

[seagle0128]

(add-to-list 'global-mode-string '(" " (:eval (assq 'proof-active-buffer-fake-minor-mode minor-mode-alist))) " ")

[vzaliva]

It worked! Thanks! In case someone else will be looking for the solution: I've added it to the hook for coq-mode in proof general use-package definition:

(use-package proof-general
  :ensure t
  :after doom-modeline
  :mode ("\\.v\\'" . coq-mode)
  :custom
  (coq-smie-user-tokens '(("≈" . "=") ("≡" . "=")))
  (proof-splash-enable nil)
  (coq-prog-name "coqtop")
  (coq-compile-before-require nil)
  :hook
  (coq-mode . (lambda ()
                (ws-butler-mode)
                (helm-mode)
                (add-to-list 'global-mode-string '(" " (:eval (assq 'proof-active-buffer-fake-minor-mode minor-mode-alist))) " ")
                )))