Show Section endings in `company-coq-occur`
vzaliva opened this issue · 3 comments
vzaliva commented
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
cpitclaudel commented
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? :)
vzaliva commented
Done. That was easy :)
cpitclaudel commented
Super, thanks a lot!