Is there a way to have unicode characters working like idents?

[beta-ziliani]

If I define a rule

(* Local Variables: *)
(* company-coq-local-symbols: ( ("_M" . ?ℳ) ) *)
(* End: *)

I would expect _M1, _M', _M_blah be printed as ℳ₁, ℳ', and ℳ_blah respectively.

Instead, I need to redefine them too as in:
("_M'" . (?ℳ (Br . Bl) ?'))

Which is far from ideal.

Is there a way to have this?

[cpitclaudel]

There is a way to have this, if we changed prettify-symbols-predicate. See the definition of company-coq-features/prettify-symbols--predicate

[beta-ziliani]

I did but I still have no clue, sorry!

[cpitclaudel]

Try this after loading company-coq, maybe?

(defconst ~/numbers '(?0 ?1 ?2 ?3 ?4 ?5 ?6 ?7 ?8 ?9))

(defun ~/prettify-symbols--same-ish-syntax (other ref)
  "Check if the syntax class of OTHER is similar to that of REF."
  (let ((stx-other (char-syntax (or other ?\s))))
    (pcase (char-syntax ref)
      (?w (and (eq stx-other ?w)
               (eq (memq ref ~/numbers) (memq other ~/numbers))))
      (?_ (eq stx-other ?_))
      (_ (memq stx-other '(?. ?\\))))))

(advice-add 'company-coq-features/prettify-symbols--same-ish-syntax
            :override #'~/prettify-symbols--same-ish-syntax)

[beta-ziliani]

It seems to work. Is there a reason not to have it by default?

In any case, I ended up coding everything in unicode (that's the reason for asking better support at fuzzy search in the first place).

[cpitclaudel]

It seems to work. Is there a reason not to have it by default?

Not sure. I could try making it the default and seeing whether people complain ^^