-
Notifications
You must be signed in to change notification settings - Fork 29
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Subscript bikeshedding #231
Comments
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.") |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Hello! This is a very selfish request, but I'd love it if there was a way to have:
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 calledB__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?
The text was updated successfully, but these errors were encountered: