Auqamacs, Proof General and company-coq

If you are using Coq under Emacs, you are most likely using Proof General (note the new link, they moved to github recently). If you are not using excellent CompanyCoq extension to PG by Clément Pit--Claudel, you certainly should! (I was wondering for a while why it is named "company". The answer is that it is based on eponymous text completion framework for Emacs. The name stands for "complete anything".)

Aquamacs is a version of Emacs popular among MacOS X users. Unfortunately some key binding from company-coq do not work under it. Specifically control-mouse-1 which should show an overlay popup with information about a clicked symbol. There is a ticket open and there is a helpful discussion with developers but it looks like we could not make it work as on other platforms. There is a workaround described below, but I am not sure if it is going to make it to official release. If it does not or until it does here is what you can do. Add the following to your .emacs:

(add-hook 'coq-mode-hook
          (lambda ()
            (company-coq-initialize) ;; Load company-coq when opening Coq files
            (if (boundp 'aquamacs-version)
                (progn 
                  (define-key company-coq-map (kbd "<c-down-mouse-3>") #'company-coq-show-definition-overlay-under-pointer)
                  (define-key company-coq-map (kbd "<c-mouse-3>") #'company-coq-clear-definition-overlay)))))

The difference from other emacsen is that you need to use control-right-mouse-click. On MacBook's touchpad it means holding Control button while clicking on touchpad with two fingers. If you are using Apple Magic Mouse, click with one finger, but on the right side of the mouse. Finally if you are using 3-button USB mouse, you should click on right button, although I have not tested this.