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

Question

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

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

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