Subscript bikeshedding

[Ptival]

Hello! This is a very selfish request, but I'd love it if there was a way to have:

A__subA_B__subB

render with the sub things being subbed, and the single central underscore visible.

My issue being, unless there's another valid separator character one may use in identifiers, I often have something called A__subA, and something called B__subB, and I want to name a lemma that relates these two.

I'd love to be able to have:
A__subA_B__subB_Prop
and
Prop_A__subA_B__subB
render with the sub things subbed, and the single underscores visible.

How hard would it be to achieve this, even if as an option not enabled by default?

[cpitclaudel]

It would not be too hard: you'd have to change the regexp used for subscripts; see this:

(defconst company-coq-features/smart-subscripts--spec
  ;; Works because '.' isn't part of symbols
  `((,(concat "\\_<" company-coq-symbol-regexp-no-dots-no-numbers "\\(_*[0-9]+\\)'*\\_>")
     (1 (company-coq-features/smart-subscripts--subscript-spec) append))
    ;; (,(concat "\\_<" company-coq-symbol-regexp-no-dots "\\(''\\)\\([0-9a-zA-Z]+\\)'*\\_>")
    ;;  (1 (company-coq-features/smart-subscripts--separator-spec) prepend)
    ;;  (2 (company-coq-features/smart-subscripts--supscript-spec) append))
    (,(concat "\\_<" company-coq-symbol-regexp-no-dots "\\(__\\)\\([a-zA-Zα-ωΑ-Ω][0-9a-zA-Zα-ωΑ-Ω]*\\)'*\\_>")
     (1 (company-coq-features/smart-subscripts--separator-spec) prepend)
     (2 (company-coq-features/smart-subscripts--subscript-spec) append)))
  "Font-lock spec for subscripts in proof script.")