cpitclaudel/company-coq

Show Section endings in `company-coq-occur`

vzaliva opened this issue · 3 comments

Pressing C-c C-, which runs the command company-coq-occur shows list of definitions along with section openings. But sections's closing End statements are omitted. This could be a little bit confusing in the case of nested sections. Also having section end present will allow jumping directly there, in case you want to add a new definition to the section.

For example, this is how it is shown now:

Section S1.
  Section S2.
      Defintion D1
      Defintion D3
  Defintion D4
Definition D5

Preffered display:

Section S1.
  Section S2.
      Defintion D1
      Defintion D3
  End S2.
  Defintion D4
End S1.
Definition D5

This is a great idea. We just need to change company-coq-named-outline-kwds to add "End" to it; do you want to make a patch? :)

Done. That was easy :)

Super, thanks a lot!