Fields of Inductive/Record/Class not available in completion

[wilcoxjay]

Consider the following code

Record foofoofoo : Type := { barbarbar : nat }.

The type foofoofoo is available in completions later in the file, but the field barbarbar is not.

The problem extends to Inductives and Classes as well.

Would it be possible to add these?

I am using coq 8.5beta2 (unpatched) with cvs trunk PG and MELPA company-coq.

Thanks for making this awesome plugin!

[cpitclaudel]

Yeah, that would be really neat ; it's a bit tricky though, because at the moment same-buffer completion only works by collecting matches of a regexp in the part of the buffer above the point, and a regexp won't work too well to match record fields. I'm currently working with the Coq team to get the patches merged, so I expect this will mostly be an issue for users of legacy versions of Coq in the future (hopefully the relevant patches will make it into the final 8.5 release).

You can use annotations to trick company-coq into seeing these fields though.

Record R : Type :=
  { Field1 : nat;
    Field2 : nat }.
(* For company-coq:
   with Field1
   with Field2 *)

But it's a bit invasive. A better way might be to adjust company-coq-defuns-regexp manually by changing your coq-mode-hook to this:

(add-hook
 'coq-mode-hook
 (lambda ()
   (company-coq-initialize)
   (setq company-coq-defuns-regexp
         (concat "\\(?:" (company-coq-make-headers-regexp company-coq-defuns-kwds company-coq-id-regexp) "\\)\\|"
                 "\\(?:(\\*\\*\\*)\\s-+\\(?2:" company-coq-id-regexp "\\)\\)"))))

which allows you to reduce the annotations to

Record R : Type := {
  (***) Field1 : nat;
  (***) Field2 : nat }.

Let me know if that works :) I'll leave this open until the patches are merged.

[wilcoxjay]

Thanks for the ideas! I'm looking forward to those patches being merged even more now.