Making it configurable to not "force" display document buffers?

[LukeXuan]

I'm using the company-box package which displays information in a childframe. It calls doc-buffer from the backend to obtain the document content, but company-coq implementation has the side effect of replacing the *goals* window with the documentation. Is it possible to add an option that only creates the buffer but does not touch the goals window?

[LukeXuan]

This is what I'm doing locally:

(defun my/company-coq-doc-buffer-generic (name cmds &optional interactive)
  "Prepare a doc buffer for NAME, using CMDS to collect information.
If INTERACTIVE is non-nil and no help is found, complain loudly."
  (company-coq-dbg "company-coq-doc-buffer-generic: Called for name %s" name)
  (-if-let* ((chapters (company-coq-doc-buffer-collect-outputs name cmds)))
      (let* ((fontized-name (propertize name 'font-lock-face 'company-coq-doc-i-face))
             (doc-tagline   (format company-coq-doc-tagline fontized-name))
             (doc-body      (mapconcat #'identity chapters company-coq-doc-def-sep))
             (doc-full      (concat doc-tagline "\n\n" doc-body))
             (buf           (get-buffer-create company-coq--doc-buffer)))
        (with-current-buffer buf
          (let ((inhibit-read-only t))
            (erase-buffer)
            (insert doc-full)
            (coq-response-mode)
            (company-coq-make-title-line 'company-coq-doc-header-face-about)
            (current-buffer))))
    (company-coq--maybe-complain-docs-not-found interactive "documentation" name)))

(advice-add 'company-coq-doc-buffer-generic :override #'my/company-coq-doc-buffer-generic)

basically, I copy-pasted the entire doc-buffer-generic definition and replaced the clean-buffer macro with with-current-buffer, so that it won't call display-in-pg-window function. I couldn't figure out an easier patch, and I'm also sure if this patch is safe or not.

[cpitclaudel]

I believe this is a variant of #221 .
I took the time to write a rough patch to support company-quickhelp in the cpc/quickhelp branch. Unfortunately I haven't had time to really try it thoroughly. Could you? If it works, you could route calls from company-box to try quick-help first, perhaps.

[LukeXuan]

I can try to reroute the call to quick-help, but I don't really use the coqdoc feature. This issue was opened because I felt it's better to fix the problem at the root rather than disabling company-box in Coq mode. Therefore I'm afriad I won't be testing it thorough enough.

[cpitclaudel]

It would be great if you tried that, yes!

This issue was opened because I felt it's better to fix the problem at the root

I'm confused: you wrote:

Is it possible to add an option that only creates the buffer but does not touch the goals window?

Isn't that what what quick-help does? Sorry if I missed something.

[LukeXuan]

Sorry I wasn't clear in my last reply. Here's the problem I'm encountering:

• I use emacs/company in a way that it attempts to show document of current completion candidate through company-box if it's idle for some time period. I rely on this feature in some other programming languages, but not really in Coq.
• When this behavior triggers in Coq mode, company-box ultimately calls doc-buffer-generic and obtains the document, with the side effect of replacing the *goals* window.

Since I don't rely on coqdoc feature, the easy fix me for is to disable this idle-auto-trigger behavior. However, I feel like it's better fixed at the root (that company-box is calling a function that changes the *goals* window).

Also since I don't rely on coqdoc feature, I'm afraid I won't test this new branch thoroughly. All I can do is to verify, whenever the documents pops up, it shows information without obvious problems.

[LukeXuan]

It seems to be working as intended. I will report back again after some usage.

[LukeXuan]

Actually, not quite right. I didn't remove the overriding scripts I had in my private config. The cpc/quickhelp branch seem to print out the content of *goals* buffer twice, here's an example

It also outputs this line of error when I first start coqtop,

company-coq: Parsing of tactic grammar failed with error (error "Top level parsing failure [(1 goal (ID 50) A : Type i (, j) : nat v : vec A i w : vec A j x : A Hcnt : i < i + S j ============================ (v +++ x ::: w) !!! nat_to_fin Hcnt = x)]").

Any idea what's going wrong here?