Глифы Unicode для ключевых слов и операторов в Coq/Proof General под Emacs

Question

Этот вопрос связан с настройкой режима Coq в Proof General в Emacs.

Я пытаюсь, чтобы Emacs автоматически заменял ключевые слова и нотацию в Coq соответствующими глифами Unicode. Мне удалось определить fun быть греческой строчной лямбда λ, forall быть универсальным символом квантора ∀ и т. д. У меня не было проблем с определением символов для слов.

Проблема в том, что когда я пытаюсь определить операторы =>, ->, <->и т. д. к их символу Unicode ⇒→↔, они не заменяются соответствующими символами Unicode в Coq. Они, однако, заменены в *scratch* буфер, когда я проверяю их. Я использую тот же механизм для сопоставления символов Unicode с обозначением Coq:

(defun define-glyph (string char-info)
  (font-lock-add-keywords
   nil
   `((,(format "\\<%s\\>" string)
      (0 (progn
       (compose-region
        (match-beginning 0) (match-end 0)
        ,(apply #'make-char char-info))
       nil))))
   ))

Я подозреваю, что проблема в том, что режим Coq помечает определенные знаки препинания как особые, поэтому Emacs игнорирует мой код и заменяет их глифами Unicode, но я не уверен. Может кто-нибудь, пожалуйста, пролить свет на это для меня?

Answer 1

Эти операторы, вероятно, являются символами, а не словами, в соответствии с таблицей синтаксиса конкретного режима. Пытаться

(defun define-glyph (string char-info)
  (font-lock-add-keywords
   nil
   `((,(format "\\_<%s\\_>" string)
      (0 (progn
           (compose-region
            (match-beginning 0) (match-end 0)
            ,(apply #'make-char char-info))
           nil))))))