Feature Request: Outline mode with TOC

[ghost]

See also: https://coq.discourse.group/t/pg-company-structured-outline-mode/798

Company/PG has the command M-x company-coq-occur (bound to C-c C-, in my case), which gives an outline of the curent lemmas/definitions/etc. However, it doesn’t follow the coqdoc structure. I use special comments to structure my script, like

(** * Title *)
(** ** Chapter *)
(** *** Section *)
(** **** etc *)

It would be nice to have an outline like this in PG/Company, like reftex's TOC (M-x reftex-toc). This would help navigating in large .v files.

[cpitclaudel]

Sure thing. The proper way to do this would probably be to move away from occur and do a proper TOC buffer, but for now you could start with changing the line that calls occur in company-coq-occur to (occur (format "\\(?:%s\\|%s\\)" company-coq-outline-regexp-base (caar company-coq-features/coqdoc--spec))). Do you want to try that?

[ghost]

I just tried that. (If the screenshot uploaded properly), you can see that there is a weird horizontal space around the headlines.

[ghost]

The screenshot was not properly uploaded, so here is what I saw in textual form:

XXX:
   :
   :
   :
   :
   :(** *** HL1 *)
   :
XXX:Definition ...
   :
   :(** *** HL2 *)
   :
XXX:Definition ...

: was displayed verbatimly, ... is omissed, XXX is a line number.